From 0fd563c07433db5aad5c5a3f196ea692bb60c04e Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 6 Jun 2017 21:22:15 +0200
Subject: [travis] extra test ci-bignums (+factorize other scripts)

---
 dev/ci/ci-math-classes.sh | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'dev/ci/ci-math-classes.sh')

diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 10b9d7af24..46581c6381 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -9,9 +9,7 @@ Corn_CI_DIR=${CI_BUILD_DIR}/corn
 
 # Setup Bignums
 
-git_checkout master https://github.com/coq/bignums.git bignums
-
-( cd bignums && make -j ${NJOBS} && make install )
+source ${ci_dir}/ci-bignums.sh
 
 # Setup Math-Classes
 
-- 
cgit v1.2.3