aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorbeta2020-06-13 17:15:12 -0300
committerThéo Zimmermann2020-06-15 17:51:14 +0200
commitd0087639010e10a6e207836c837b7f61c9cb2e55 (patch)
tree22633503e69a5daf5c0ce7485f9c628299abef8d /dev
parent13e8d04b2f080fbc7ca169bc39e53c8dd091d279 (diff)
updated ci for unicoq
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh2
-rwxr-xr-xdev/ci/ci-unicoq.sh2
2 files changed, 2 insertions, 2 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 9737e1b2e0..cdf00f4767 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -31,7 +31,7 @@
########################################################################
# Unicoq + Mtac2
########################################################################
-: "${unicoq_CI_REF:=68ed13294ea8860a8c39950f7ca2ff0aa7211b9f}"
+: "${unicoq_CI_REF:=master}"
: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}"
: "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-unicoq.sh b/dev/ci/ci-unicoq.sh
index 36acb115e9..df1d9cceb8 100755
--- a/dev/ci/ci-unicoq.sh
+++ b/dev/ci/ci-unicoq.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
git_download unicoq
-( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install )
+( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f _CoqProject -o Makefile && make && make install )