diff options
| author | Enrico Tassi | 2020-11-24 10:08:05 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-11-25 15:58:31 +0100 |
| commit | 94abc3dce396b77e98900e604e3117986dd2ab60 (patch) | |
| tree | 6ff0e208249d6e4611285abf1e067eb96e79c166 /dev/ci/ci-basic-overlay.sh | |
| parent | 572f48a57987100ad3aa98fc4c5187c6e22c7232 (diff) | |
[ci] job for menhir
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 75d9efaadc..18fdd83218 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -306,7 +306,7 @@ # menhirlib ######################################################################## # Note: menhirlib is now in subfolder coq-menhirlib of menhir -: "${menhirlib_CI_REF:=master}" +: "${menhirlib_CI_REF:=20201122}" : "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/menhir}" : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" |