aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEnrico Tassi2020-03-11 16:07:39 +0100
committerGitHub2020-03-11 16:07:39 +0100
commitc259b25089a159c5c86a940c7dc27a1abfd90498 (patch)
tree4c05b5d9acb9b371cf043613c552c9a16363dd2e /dev
parent3781d8b24d2076f81ec7470bfcde9ab218331400 (diff)
Update dev/ci/ci-basic-overlay.sh
Co-Authored-By: Gaƫtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index e308ca4866..bd7ee46358 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -219,6 +219,7 @@
: "${elpi_CI_REF:=coq-master}"
: "${elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}"
: "${elpi_CI_ARCHIVEURL:=${elpi_CI_GITURL}/archive}"
+
: "${elpi_hb_CI_REF:=coq-master}"
: "${elpi_hb_CI_GITURL:=https://github.com/math-comp/hierarchy-builder}"
: "${elpi_hb_CI_ARCHIVEURL:=${elpi_hb_CI_GITURL}/archive}"