From a0c84abf1f3078c1ba42df1b588acbac4bc2e4df Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 6 Jun 2017 14:20:52 -0400
Subject: 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.
---
 dev/ci/ci-unimath.sh | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'dev/ci/ci-unimath.sh')

diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 66b56add77..10fd56d11e 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" )
-- 
cgit v1.2.3