diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-16 13:37:43 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-17 18:41:06 +0200 |
| commit | 3b089a920181aa6b6b959fc13ac86383f1c48198 (patch) | |
| tree | 0a85107948354611e35479dd985b78cdb8441041 /.circleci | |
| parent | 5281317cb558f2b9aa6f854b9c7aeb617beba8e6 (diff) | |
[circle] Use Docker image from Gitlab registry.
Diffstat (limited to '.circleci')
| -rw-r--r-- | .circleci/config.yml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 79f83d472..4d2fb1a4d 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -8,10 +8,11 @@ defaults: # reference syntax) working_directory: ~/coq docker: - - image: coqci/base:V2018-05-07-V2 + - image: $CI_REGISTRY_IMAGE:$CACHEKEY environment: &envvars - NATIVE_COMP: "yes" + CACHEKEY: "bionic_coq-V2018-05-07-V2" + CI_REGISTRY_IMAGE: registry.gitlab.com/coq/coq version: 2 @@ -46,7 +47,9 @@ before_script: &before_script paths: - coq/ - environment: *envvars + environment: + <<: *envvars + NATIVE_COMP: "yes" .ci-template: &ci-template <<: *params @@ -63,6 +66,7 @@ before_script: &before_script root: *workspace paths: - coq/ + environment: *envvars # Defines individual jobs, see the workflows section below for job orchestration jobs: |