aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-basic-overlay.sh
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/ci/ci-basic-overlay.sh
parentb5ad6a80107f196fa8ffcc4f5dff58bea8c4f70e (diff)
parent032e4f2bf5cb6eadba6ebbb16dd5d0c812dd2033 (diff)
Merge branch 'v8.7'
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
-rw-r--r--dev/ci/ci-basic-overlay.sh4
1 files changed, 2 insertions, 2 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