From 37980b4f3d3a1e3da5a4dc5c70265e42d1ac2ca2 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 13 Dec 2017 13:24:19 +0100 Subject: [PATCH] update README --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 3e648168..dc8bd6a3 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. -- GitLab