diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-07-15 15:23:02 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-07-21 15:02:46 +0200 |
| commit | 6ea07bb51a935e8f6292a1c84b55cb7a273a6c70 (patch) | |
| tree | f82c647e536631900f1ff23f629a6149db2c1fe1 /.gitlab-ci.yml | |
| parent | 4d858df22bb30d2efbef39a177c28c15c600c885 (diff) | |
Add [opam update] and online repository to gitlab CI script.
This allows it to find out about new packages / compilers without
having to invalidate cache somehow.
Additionally the latest camlp5 (7.01) is not in the local repository
for some reason.
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8b43d975a..b47494d3a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -40,6 +40,11 @@ before_script: - if [ ! "(" -d .opamcache ")" ]; then mv ~/.opam .opamcache; else mv ~/.opam ~/.opam-old; fi - ln -s $(readlink -f .opamcache) ~/.opam + # the default repo in this docker image is a local directory + # at the time of 4aaeb8abf it lagged behind the official + # repository such that camlp5 7.01 was not available + - opam repository set-url default https://opam.ocaml.org + - opam update - opam switch ${COMPILER} - eval $(opam config env) - opam config list |