diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-20 10:17:18 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-20 10:17:18 -0700 |
| commit | 817790844673724a13ccdbbf509e1d2885f4d293 (patch) | |
| tree | 7d096eca966f68e363368b54bcc3b2510dd200f9 /.travis.yml | |
| parent | 79e6c4ea6cd0ed52fda2168cda78c52e4bc4896a (diff) | |
Display pretty timing graph on travis
Diffstat (limited to '.travis.yml')
| -rw-r--r-- | .travis.yml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.travis.yml b/.travis.yml index 59fbead87..ae5ed9645 100644 --- a/.travis.yml +++ b/.travis.yml @@ -32,4 +32,4 @@ before_install: - sudo apt-get update -q - sudo apt-get install $COQ_PACKAGE -y -script: make COQPATH="$(pwd)/$COQPRIME" TIMED=1 -j2 +script: COQPATH="$(pwd)/$COQPRIME" ./etc/coq-scripts/timing/make-pretty-timed.sh -j2 && make COQPATH="$(pwd)/$COQPRIME" TIMED=1 -j2 |