diff --git a/README.md b/README.md index 3e648168dd1b0d425fe742bad0992c566070776c..dc8bd6a3ecea2b4b7df1d5aa76dd482c6e68458f 100644 --- a/README.md +++ b/README.md @@ -25,7 +25,7 @@ After doing `git pull`, the development may fail to compile because of outdated dependencies. To fix that, please run `opam update` followed by `make build-dep`. -## Building Instructions +## Building Run `make -jN` to build the full development, where `N` is the number of your CPU cores.