From ee42eb1e10be8632e277cf8b9ac6ba40ef86372b Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Fri, 6 Oct 2017 14:08:49 +0200
Subject: travis: remove the overlay on bignums

 This overlay is now useless (change pushed upstream in bignums) and
 moreover does not contain my commit making bignums resilient to PR#768.
---
 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..baca14dff2 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}
-- 
cgit v1.2.3