diff options
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 |