diff options
Diffstat (limited to 'dev/ci/ci-common.sh')
| -rw-r--r-- | dev/ci/ci-common.sh | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index f1e1515d41..238960948d 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -18,7 +18,9 @@ ls "$COQBIN" # Where we clone and build external developments CI_BUILD_DIR=`pwd`/_build_ci -source ${ci_dir}/ci-user-overlay.sh +for overlay in ${ci_dir}/user-overlays/*.sh; do + source ${overlay} +done source ${ci_dir}/ci-basic-overlay.sh mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp @@ -66,7 +68,7 @@ install_ssreflect() sed -i.bak '/field/d' Make && \ sed -i.bak '/fingroup/d' Make && \ sed -i.bak '/algebra/d' Make && \ - make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install ) + make Makefile.coq && make -f Makefile.coq all && make install ) echo -en 'travis_fold:end:ssr.install\\r' |