From c04536a44bd55d6ddef3ed4f3bf2c3a1dd3bb258 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 4 Oct 2017 10:08:35 +0200
Subject: [ci] Remove temporary bignums overlay.

---
 dev/ci/ci-basic-overlay.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 8e7265969b..43525dcd40 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -127,5 +127,5 @@
 ########################################################################
 # Bignums
 ########################################################################
-: ${bignums_CI_BRANCH:=fix-thunk-printer}
-: ${bignums_CI_GITURL:=https://github.com/ppedrot/bignums.git}
+: ${bignums_CI_BRANCH:=master}
+: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git}
-- 
cgit v1.2.3