From 0bb73fb7e421f6778826be1ba699d02df7872ec0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 5 Oct 2017 10:05:55 +0200
Subject: [PATCH] explain make parallelism

---
 README.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 92f69e042..251213b6e 100644
--- a/README.md
+++ b/README.md
@@ -30,7 +30,8 @@ dependencies.  To fix that, please run `opam update` followed by
 
 ## Building Instructions
 
-Run `make` to build the full development.
+Run `make -jN` to build the full development, where `N` is the number of your
+CPU cores.
 
 ## Structure
 
-- 
GitLab