aboutsummaryrefslogtreecommitdiffhomepage
path: root/.circleci
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-31 07:45:03 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-31 07:45:03 +0100
commitc658141acff6d1b7f610960dd39998385c7e8806 (patch)
tree81202ba81139cc62438442b3a3d3b14bfd7fee5e /.circleci
parent556360215c910c8ae6d14b3582330fda055fff53 (diff)
parentec81b54bc04efd5f101d127cc80c43c268e69fcd (diff)
Merge PR #6601: Circle CI: fix cache selection.
Diffstat (limited to '.circleci')
-rw-r--r--.circleci/config.yml13
1 files changed, 10 insertions, 3 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml
index c49bc3b08..9b0cc2119 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -54,10 +54,17 @@ opam-switch: &opam-switch
steps:
- checkout
- run: *before_script
+ - run:
+ name: Cache selection
+ command: |
+ source ~/.profile
+ # We can't use environment variables in cache names
+ # So put it in a file and use the checksum
+ echo "$COMPILER" > COMPILER
- restore_cache:
keys:
- - coq-opam-cache-v1-{{ arch }}-{{ .Environment.COMPILER }}-{{ checksum ".circleci/config.yml" }}-
- - coq-opam-cache-v1-{{ arch }}-{{ .Environment.COMPILER }}- # this grabs old cache if checksum doesn't match
+ - coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}-
+ - coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}- # this grabs old cache if checksum doesn't match
- run:
name: Update opam lists
command: |
@@ -76,7 +83,7 @@ opam-switch: &opam-switch
source ~/.profile
rm -rf ~/.opam/log/
- save_cache:
- key: coq-opam-cache-v1-{{ arch }}-{{ .Environment.COMPILER }}-{{ checksum ".circleci/config.yml" }}-
+ key: coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}-
paths:
- ~/.opam
- persist_to_workspace: