diff options
author | 2017-06-06 14:20:52 -0400 | |
---|---|---|
committer | 2017-07-21 03:36:47 -0400 | |
commit | a0c84abf1f3078c1ba42df1b588acbac4bc2e4df (patch) | |
tree | d332b59ee24266c02394715c5653e83ed4b9e00d /dev/ci/ci-unimath.sh | |
parent | 4d858df22bb30d2efbef39a177c28c15c600c885 (diff) |
Display timing data travis for various projects
HoTT, which builds it's own makefile, and supports timing data, makes
use of its own timing script.
Everything else goes through the coq-bundled timing scripts.
Diffstat (limited to 'dev/ci/ci-unimath.sh')
-rwxr-xr-x | dev/ci/ci-unimath.sh | 3 |
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" ) |