aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMaxime Dénès2017-07-11 14:44:59 +0200
committerMaxime Dénès2017-07-11 14:44:59 +0200
commit0986ee250818a5cb517b5e59fbd31e2cd1667775 (patch)
tree01d38409f9db6202aabe16249df7d489cd853920 /dev
parentb5ad6a80107f196fa8ffcc4f5dff58bea8c4f70e (diff)
parent032e4f2bf5cb6eadba6ebbb16dd5d0c812dd2033 (diff)
Merge branch 'v8.7'
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/ci-basic-overlay.sh4
-rwxr-xr-xdev/ci/ci-compcert.sh3
2 files changed, 4 insertions, 3 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 99ec43e412..91337b9013 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -91,8 +91,8 @@
########################################################################
# fiat_crypto
########################################################################
-: ${fiat_crypto_CI_BRANCH:=less_init_plugins}
-: ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git}
+: ${fiat_crypto_CI_BRANCH:=master}
+: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
########################################################################
# formal-topology
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 0dd904648c..4cfe0911b6 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -9,4 +9,5 @@ opam install -j ${NJOBS} -y menhir
git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
# Patch to avoid the upper version limit
-( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make )
+( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make )
+