diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-13 15:05:10 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-13 15:05:10 +0100 |
| commit | cef0430e14c370e6cbfe72db75e61cb4b8c8a8b9 (patch) | |
| tree | 7fdfa7c402273e7886cd8077a027cf8f263812d1 /.circleci | |
| parent | 4d11d6dc3bfcef3ecdf3f905dcf2fdbca259677e (diff) | |
Circle CI: enable TIMED for external developments
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 |