diff options
| author | Maxime Dénès | 2017-07-26 15:24:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-26 15:24:35 +0200 |
| commit | 941f92a8b623b3d79fb0802e0b47709a7b50f275 (patch) | |
| tree | 1db8277e8e3f933d21f187b55bdd31eafed9fb94 | |
| parent | cacb8a5c32eddf7d24364e0de60f5fbe652fab6c (diff) | |
| parent | 6ea07bb51a935e8f6292a1c84b55cb7a273a6c70 (diff) | |
Merge PR #910: Add [opam update] and online repository to gitlab CI script.
| -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 8b43d975ac..b47494d3ae 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 |