diff options
| author | Alasdair | 2020-06-03 14:44:21 +0100 |
|---|---|---|
| committer | Alasdair | 2020-06-03 14:44:21 +0100 |
| commit | 8ad94340837ecd1d83a07e1de540c605f22f329c (patch) | |
| tree | 436d6e45d9977b375196600f7f81e6a676ba25df /etc | |
| parent | dc4fe34905891510b7fd7d3b9fb86af49ce89879 (diff) | |
Correct compiler version in CI script
Diffstat (limited to 'etc')
| -rwxr-xr-x | etc/ci_opam_latest_build.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/etc/ci_opam_latest_build.sh b/etc/ci_opam_latest_build.sh index 13fbe0ac..9e994b22 100755 --- a/etc/ci_opam_latest_build.sh +++ b/etc/ci_opam_latest_build.sh @@ -2,7 +2,7 @@ set -eu -opam init -y --no-setup --compiler=4.10 --shell=sh +opam init -y --no-setup --compiler=4.10.0 --shell=sh eval `opam config env` |