11 files changed, 31 insertions, 45 deletions
diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh
index d68674381a..c90e516ae9 100755
--- a/dev/ci/ci-bignums.sh
+++ b/dev/ci/ci-bignums.sh
@@ -13,4 +13,4 @@ bignums_CI_DIR=${CI_BUILD_DIR}/Bignums
 
 git_checkout ${bignums_CI_BRANCH} ${bignums_CI_GITURL} ${bignums_CI_DIR}
 
-( cd ${bignums_CI_DIR} && make -j ${NJOBS} && make install)
+( cd ${bignums_CI_DIR} && make && make install)
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index c3ae7552a9..558e8cbb8c 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -5,9 +5,6 @@ source ${ci_dir}/ci-common.sh
 
 CoLoR_CI_DIR=${CI_BUILD_DIR}/color
 
-# Setup Bignums
-source ${ci_dir}/ci-bignums.sh
-
 # Compile CoLoR
 git_checkout ${CoLoR_CI_BRANCH} ${CoLoR_CI_GITURL} ${CoLoR_CI_DIR}
 ( cd ${CoLoR_CI_DIR} && make )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 1bfdf7dfbe..23131c94c6 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -53,6 +53,18 @@ checkout_mathcomp()
   git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1}
 }
 
+make()
+{
+    # +x: add x only if defined
+    if [ -z "${MAKEFLAGS+x}" ] && [ -n "${NJOBS}" ];
+    then
+        # Not submake and parallel make requested
+        command make -j "$NJOBS" "$@"
+    else
+        command make "$@"
+    fi
+}
+
 # this installs just the ssreflect library of math-comp
 install_ssreflect()
 {
diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh
index b610f70004..5d6bd6a368 100755
--- a/dev/ci/ci-coq-dpdgraph.sh
+++ b/dev/ci/ci-coq-dpdgraph.sh
@@ -7,4 +7,4 @@ coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph
 
 git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR}
 
-( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make test-suite )
+( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make && make test-suite )
diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh
new file mode 100755
index 0000000000..54cad5df4c
--- /dev/null
+++ b/dev/ci/ci-corn.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Corn_CI_DIR=${CI_BUILD_DIR}/corn
+
+git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
+
+( cd ${Corn_CI_DIR} && make && make install )
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index f7470463d9..62854afac6 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -7,4 +7,4 @@ Equations_CI_DIR=${CI_BUILD_DIR}/Equations
 
 git_checkout ${Equations_CI_BRANCH} ${Equations_CI_GITURL} ${Equations_CI_DIR}
 
-( cd ${Equations_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} && make -j ${NJOBS} test-suite && make -j ${NJOBS} examples && make install)
+( cd ${Equations_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make && make test-suite && make examples && make install)
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index 2556f84a55..53eb55fc45 100755
--- a/dev/ci/ci-formal-topology.sh
+++ b/dev/ci/ci-formal-topology.sh
@@ -3,30 +3,8 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
-
-Corn_CI_DIR=${CI_BUILD_DIR}/corn
-
 formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology
 
-# Setup Bignums
-
-source ${ci_dir}/ci-bignums.sh
-
-# Setup Math-Classes
-
-git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
-
-( cd ${math_classes_CI_DIR} && make && make install )
-
-# Setup Corn
-
-git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
-
-( cd ${Corn_CI_DIR} && make && make install )
-
-# Setup formal-topology
-
 git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR}
 
 ( cd ${formal_topology_CI_DIR} && make )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 1bf6e9a872..693135a4c9 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 )
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 )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 2837dee963..db4a31e549 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -5,20 +5,6 @@ source ${ci_dir}/ci-common.sh
 
 math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
 
-Corn_CI_DIR=${CI_BUILD_DIR}/corn
-
-# Setup Bignums
-
-source ${ci_dir}/ci-bignums.sh
-
-# Setup Math-Classes
-
 git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
 
 ( cd ${math_classes_CI_DIR} && make && make install )
-
-# Setup Corn
-
-git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
-
-( cd ${Corn_CI_DIR} && make )
diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
index 96acc5a11c..12a70176c2 100755
--- a/dev/ci/ci-wrapper.sh
+++ b/dev/ci/ci-wrapper.sh
@@ -13,11 +13,14 @@ function travis_fold {
     fi
 }
 
-CI_SCRIPT="$1"
+CI_NAME="$1"
+CI_SCRIPT="ci-${CI_NAME}.sh"
+
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 # assume this script is in dev/ci/, cd to the root Coq directory
 cd "${DIR}/../.."
 
+export TIMED=1
 "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log
 travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...'
 python ./tools/make-one-time-file.py time-of-build.log