From eb91eb5dd0487493b0b2e1a62ccabf4c8115ac98 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 6 Mar 2018 05:18:18 -0800
Subject: Hack to make bignum build on windows

---
 dev/build/windows/makecoq_mingw.sh | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev/build')

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 49eece5a4..bea30b1a7 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1337,6 +1337,8 @@ function make_coq_installer {
 
 function make_addon_bignums {
   if build_prep https://github.com/coq/bignums/archive/ master zip 1 bignums-8.8.0; then
+    # To make command lines shorter :-(
+    echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local
     logn make make all
     logn make-install make install
     build_post
-- 
cgit v1.2.3