From fface0eef97f9a9d9c4dbf193598909b0a62e6ca Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 23 Jan 2018 15:44:07 +0100
Subject: Put default value for NJOBS in ci-common.

---
 dev/ci/ci-common.sh | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'dev/ci/ci-common.sh')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 1838db5d01..05fa33e972 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -2,6 +2,10 @@
 
 set -xe
 
+# default value for NJOBS
+: "${NJOBS:=1}"
+export NJOBS
+
 if [ -n "${GITLAB_CI}" ];
 then
     export COQBIN="$PWD/_install_ci/bin"
-- 
cgit v1.2.3