aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEnrico Tassi2020-03-11 14:38:29 +0100
committerEnrico Tassi2020-03-11 14:38:29 +0100
commit3781d8b24d2076f81ec7470bfcde9ab218331400 (patch)
treee1c0d457afc0d2ac0600327d1d2ce7eabe7eb862 /dev
parent45e83041ee129a541fdf17a8c50dd6e9e0e81262 (diff)
[CI] test hierarchy builder as part of elpi
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh5
-rwxr-xr-xdev/ci/ci-elpi.sh4
2 files changed, 8 insertions, 1 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 60c266699c..e308ca4866 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -214,11 +214,14 @@
: "${equations_CI_ARCHIVEURL:=${equations_CI_GITURL}/archive}"
########################################################################
-# Elpi
+# Elpi + Hierarchy Builder
########################################################################
: "${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}"
########################################################################
# fcsl-pcm
diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh
index d60bf34ba2..4f185db813 100755
--- a/dev/ci/ci-elpi.sh
+++ b/dev/ci/ci-elpi.sh
@@ -6,3 +6,7 @@ ci_dir="$(dirname "$0")"
git_download elpi
( cd "${CI_BUILD_DIR}/elpi" && make && make install )
+
+git_download elpi_hb
+
+( cd "${CI_BUILD_DIR}/elpi_hb" && make && make install )