diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 11:32:00 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 11:32:00 +0200 |
| commit | e33cd69ab6fcb38478a6c0e00628a5de16181906 (patch) | |
| tree | a5783d1d8a77483585dcd1bb1eaad9fa155f10e2 /dev/build | |
| parent | 36c950f8a6f70b9b70aecc3e4a620b969ca6a0e0 (diff) | |
| parent | 6729388e9f51d7efb86ac64d10cc3eb4fffe44a0 (diff) | |
Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META file
Diffstat (limited to 'dev/build')
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index f3e4cec0b..f12cbe0a7 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -910,6 +910,10 @@ function make_camlp5 { log2 make install # For some reason gramlib.a is not copied, but it is required by Coq cp lib/gramlib.a "$PREFIXOCAML/libocaml/camlp5/" + # For some reason META is not copied, but it is required by coq_makefile + log2 make -C etc META + mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/" + cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/" log2 make clean build_post fi |