diff options
| author | Emilio Jesus Gallego Arias | 2020-03-14 17:38:28 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-16 19:55:14 -0400 |
| commit | d1e47163f50b1b190412f1b3bd4f74aac5829f0a (patch) | |
| tree | 54e792f677459aec072d43de66230f465b911459 /.gitlab-ci.yml | |
| parent | 901cbfab468efa868e3838c2009ac09978ee661a (diff) | |
[ci] [docker] Update components in Docker image
We bump ounit, odoc, and lablgtk3 ; so far this is routine maintenance.
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 68bb24ac77..5aa0fee16f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2019-03-01-V43" + CACHEKEY: "bionic_coq-V2019-03-14-V14" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" |