diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-19 10:46:34 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-19 10:46:34 +0100 |
| commit | ec81b54bc04efd5f101d127cc80c43c268e69fcd (patch) | |
| tree | 33cb5301067daac0e17edeec7b1790b4d06f376a /.circleci | |
| parent | f431dac2e219cb2a76b22e452d6e407869d89f42 (diff) | |
Circle CI: fix cache selection.
Diffstat (limited to '.circleci')
| -rw-r--r-- | .circleci/config.yml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 7c250c667..27519eab2 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: |