diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-09-04 15:37:00 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-09-07 12:48:18 +0200 |
| commit | 6729388e9f51d7efb86ac64d10cc3eb4fffe44a0 (patch) | |
| tree | e1b01250d7ca70490f483136e63d0490b54439ed /dev/build | |
| parent | cb2d69efa4d012a6828077675aba1d2a51d710ef (diff) | |
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 |