From 08e86c0af77e83b8569fe611b9fb74e772d710a8 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Tue, 6 Jun 2017 20:47:26 +0200
Subject: [travis] overlay + extra deps for math-classes (and formal-topology)

---
 dev/ci/ci-formal-topology.sh | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'dev/ci/ci-formal-topology.sh')

diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index ecb36349f..87171ba0b 100755
--- a/dev/ci/ci-formal-topology.sh
+++ b/dev/ci/ci-formal-topology.sh
@@ -9,6 +9,12 @@ Corn_CI_DIR=${CI_BUILD_DIR}/corn
 
 formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology
 
+# Setup Bignums
+
+git_checkout master https://github.com/coq/bignums.git bignums
+
+( cd bignums && make -j ${NJOBS} && make install )
+
 # Setup Math-Classes
 
 git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
-- 
cgit v1.2.3