diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-03-06 05:18:18 -0800 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-03-06 05:56:48 -0800 |
| commit | eb91eb5dd0487493b0b2e1a62ccabf4c8115ac98 (patch) | |
| tree | ab723caabf1f1bcdbc5438128928f847f83e002d /dev/build | |
| parent | 951f80b0ce46976791d8b7fa7cf68aea11018da0 (diff) | |
Hack to make bignum build on windows
Diffstat (limited to 'dev/build')
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 2 |
1 files changed, 2 insertions, 0 deletions
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 |