aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-hott.sh
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-12-19 15:54:34 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-12-21 00:07:34 +0100
commitcf04e49c5426da3ea684f8e545652803106af0c2 (patch)
tree394baab9d1aff785f2eef7b75f9297a07c286a7c /dev/ci/ci-hott.sh
parentf431dac2e219cb2a76b22e452d6e407869d89f42 (diff)
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.
Diffstat (limited to 'dev/ci/ci-hott.sh')
-rwxr-xr-xdev/ci/ci-hott.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 1bf6e9a87..693135a4c 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -7,4 +7,4 @@ HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT
git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR}
-( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} )
+( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make )