diff options
| -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 |