diff options
Diffstat (limited to 'dev/ci/ci-unimath.sh')
| -rwxr-xr-x | dev/ci/ci-unimath.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 175b82b5f9..66b56add77 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -10,5 +10,5 @@ git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR} ( cd ${UniMath_CI_DIR} && \ sed -i.bak '/Folds/d' Makefile && \ sed -i.bak '/HomologicalAlgebra/d' Makefile && \ - make -j ${NJOBS} BUILD_COQ=no ) + make BUILD_COQ=no ) |