From cef0430e14c370e6cbfe72db75e61cb4b8c8a8b9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 13 Dec 2017 15:05:10 +0100
Subject: Circle CI: enable TIMED for external developments

---
 .circleci/config.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to '.circleci')

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
-- 
cgit v1.2.3