aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-basic-overlay.sh
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-07 12:44:47 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-07 12:44:47 +0200
commit084ef41c98d52078f85831c940d0a073a4ccdb7a (patch)
treef1808d72e562f0dd674759f2f447f44cd5da9aad /dev/ci/ci-basic-overlay.sh
parent276f08cb053eed175478c4c9359e61fb949742ba (diff)
parent1db568d3dc88d538f975377bb4d8d3eecd87872c (diff)
Merge PR #914: Making the detyper lazy
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 43525dcd4..8e7265969 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -127,5 +127,5 @@
########################################################################
# Bignums
########################################################################
-: ${bignums_CI_BRANCH:=master}
-: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git}
+: ${bignums_CI_BRANCH:=fix-thunk-printer}
+: ${bignums_CI_GITURL:=https://github.com/ppedrot/bignums.git}