From bba2186f781695db9d0987758119fde061499fbc Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 12:44:01 +0200
Subject: [travis] fix Software Foundation (one added Require Extraction)

---
 dev/ci/ci-sf.sh | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 7d23ccad97..23ef41d2dd 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -7,6 +7,8 @@ source ${ci_dir}/ci-common.sh
 wget ${sf_CI_TARURL}
 tar xvfz sf.tgz
 
+sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v
+
 ( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} )
 
 
-- 
cgit v1.2.3