diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-05 19:23:49 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-07 20:23:17 +0200 |
| commit | cde263581c49a75f8abdbcb398511942906e6204 (patch) | |
| tree | 615d8c5f4e824aeaeec7a8ce317638fe41cd8355 /.circleci | |
| parent | 612ca9e742c3196ea5faad100bb95d9e08ebe07e (diff) | |
[gitlab] Add bleeding-edge flambda build.
We also introduce a bit more systematic job naming: `base/edge`.
In order to make the flambda switch selectable we update the Docker
image so all the dependencies are installed in that one.
Note the extra quote rule for the flambda parameters, but unless we
can assign arrays to Gitlab variables there is not a good way to do
this I'm afraid.
With this patch we are getting close to being able to remove most
builds from Travis.
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 c4b7733a6..892175381 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-07 + - image: coqci/base:V2018-05-07-V2 environment: &envvars NATIVE_COMP: "yes" |