diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-01-31 07:45:03 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-31 07:45:03 +0100 |
commit | c658141acff6d1b7f610960dd39998385c7e8806 (patch) | |
tree | 81202ba81139cc62438442b3a3d3b14bfd7fee5e /.circleci | |
parent | 556360215c910c8ae6d14b3582330fda055fff53 (diff) | |
parent | ec81b54bc04efd5f101d127cc80c43c268e69fcd (diff) |
Merge PR #6601: 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 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: |