diff options
| author | Michael Soegtrop | 2018-05-19 11:38:16 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2018-05-19 11:38:16 +0200 |
| commit | 6ff355338986e87f37ad25bf9943ca42135357d6 (patch) | |
| tree | 0d368a2ee357e12bb23ea236808d85597613c1f2 /dev | |
| parent | e0131a0038531ccc5f42fa84c79761a364b10dd7 (diff) | |
| parent | 1c5f120fba49b397aad7b8c07dcc10cec1cfc026 (diff) | |
Merge PR #7527: [windows] Don't build menhir and int anymore in the packaging scripts.
Diffstat (limited to 'dev')
| -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 3608f7305d..ecc45735f1 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 ##### |