diff options
Diffstat (limited to '.circleci')
| -rw-r--r-- | .circleci/config.yml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 7b68a0711..718bd6b5e 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -218,7 +218,7 @@ before_script: &before_script command: | source ~/.profile echo 'start:coq.test' - make -f Makefile.ci -j ${NJOBS} ${CIRCLE_JOB} + make -f Makefile.ci -j ${NJOBS} TIMED=1 ${CIRCLE_JOB} echo 'end:coq.test' environment: &ci-template-vars <<: *envvars |