diff options
Diffstat (limited to 'dev/ci/ci-equations.sh')
| -rwxr-xr-x | dev/ci/ci-equations.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index f7470463d..62854afac 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) |