From cf04e49c5426da3ea684f8e545652803106af0c2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 19 Dec 2017 15:54:34 +0100
Subject: Fix CI with parallel make (messed up dependencies)

When invoking through Makefile we always rebuild dependencies. To skip
dependencies, invoke ci-wrapper directly. We make Circle CI do this.

In order to properly support invoking ci-wrapper directly we replace
"make" in ci-common by a bash function which adds -j to the make
invocation outside submakes. We also set TIMED in the ci-wrapper.
---
 dev/ci/ci-ltac2.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh
index ed40036012..820ff89eec 100755
--- a/dev/ci/ci-ltac2.sh
+++ b/dev/ci/ci-ltac2.sh
@@ -7,4 +7,4 @@ ltac2_CI_DIR=${CI_BUILD_DIR}/ltac2
 
 git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR}
 
-( cd ${ltac2_CI_DIR} && make -j ${NJOBS} && make tests && make install )
+( cd ${ltac2_CI_DIR} && make && make tests && make install )
-- 
cgit v1.2.3