diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-16 13:40:28 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-16 13:40:28 +0200 |
| commit | 1c5f120fba49b397aad7b8c07dcc10cec1cfc026 (patch) | |
| tree | dd6c4772165cdc4f546105c5486476611d34c9b9 /dev/build | |
| parent | 3f480c993311d19b152deb6bb4dc561188d76fc7 (diff) | |
[windows] Don't make menhir and int anymore.
As pointed out by @MSoegtropIMC
[here](https://github.com/coq/coq/pull/7522#issuecomment-389478963)
there are not needed to build the packages, so not building them will
save a couple of minutes.
Diffstat (limited to 'dev/build')
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 3608f7305..ecc45735f 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -847,7 +847,7 @@ function make_ocaml { function make_ocaml_tools { make_findlib - make_menhir + # make_menhir make_camlp5 } @@ -856,7 +856,7 @@ function make_ocaml_tools { function make_ocaml_libs { make_findlib make_lablgtk - make_stdint + # make_stdint } ##### FINDLIB Ocaml library manager ##### |