diff options
| author | Jason Gross | 2017-06-11 20:22:43 -0400 |
|---|---|---|
| committer | GitHub | 2017-06-11 20:22:43 -0400 |
| commit | 75f42c5c4f350f301ef1968459f4f19f7a349ad4 (patch) | |
| tree | 272ca2e26030fe1d4e487c68db3b0444ef4de29d /dev/ci/ci-basic-overlay.sh | |
| parent | 79c42e22dd5106dcb85229ceec75331029ab5486 (diff) | |
Point ci-hott at a newer version of HoTT
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index a6972c9500..d75011de3f 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -46,8 +46,8 @@ ######################################################################## # HoTT ######################################################################## -# Temporal overlay -: ${HoTT_CI_BRANCH:=mz-8.7} +# Temporary overlay +: ${HoTT_CI_BRANCH:=ocaml.4.02.3} : ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git} # : ${HoTT_CI_BRANCH:=master} # : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git} |