aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-unimath.sh
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci/ci-unimath.sh')
-rwxr-xr-xdev/ci/ci-unimath.sh3
1 files changed, 1 insertions, 2 deletions
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 66b56add7..10fd56d11 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -10,5 +10,4 @@ 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 BUILD_COQ=no )
-
+ make BUILD_COQ=no pretty-timed TGTS="all" )