From 3b089a920181aa6b6b959fc13ac86383f1c48198 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 16 May 2018 13:37:43 +0200 Subject: [circle] Use Docker image from Gitlab registry. --- .gitlab-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to '.gitlab-ci.yml') diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c010da4cf..07777441f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: bionic_coq-V2018-05-07-V2 + CACHEKEY: "bionic_coq-V2018-05-07-V2" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" -- cgit v1.2.3