aboutsummaryrefslogtreecommitdiffhomepage
path: root/.circleci
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-05-07 15:30:38 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-05-07 15:30:38 +0200
commit612ca9e742c3196ea5faad100bb95d9e08ebe07e (patch)
tree3129f7390a325b386acb3c88fab1bab21954791e /.circleci
parenta8985ab0e8cebb8b06ff6680ac65121357448076 (diff)
parent52caadda3674c126cbec014f0727e696278868f3 (diff)
Merge PR #7445: [ci] Add ounit to the base Docker package set.
Diffstat (limited to '.circleci')
-rw-r--r--.circleci/config.yml2
1 files changed, 1 insertions, 1 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml
index 07b728edf..c4b7733a6 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -8,7 +8,7 @@ defaults:
# reference syntax)
working_directory: ~/coq
docker:
- - image: coqci/base:V2018-05-05
+ - image: coqci/base:V2018-05-07
environment: &envvars
NATIVE_COMP: "yes"