From fe972a369adf533e2f4ec89eafb63b08a26e2ec7 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 6 Jun 2017 19:45:48 +0200
Subject: [travis] adapt CoLoR compilation to depend on the bignum package

---
 dev/ci/ci-color.sh | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 3f0716511d..cb212e845c 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -5,6 +5,19 @@ source ${ci_dir}/ci-common.sh
 
 Color_CI_DIR=${CI_BUILD_DIR}/color
 
+# Setup Bignums
+
+git_checkout master https://github.com/coq/bignums.git bignums
+
+( cd bignums && make -j ${NJOBS} && make install )
+
+# Compiles CoLoR
+
 svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR}
 
+sed -i -e "s/From Coq Require Import BigN/From Bignums Require Import BigN/" ${Color_CI_DIR}/Util/*/*.v
+sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${Color_CI_DIR}/Util/*/*.v
+sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v
+sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v
+
 ( cd ${Color_CI_DIR} && make -j ${NJOBS} )
-- 
cgit v1.2.3