diff options
| author | Gaëtan Gilbert | 2018-05-14 14:31:59 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-14 14:31:59 +0200 |
| commit | 2dcc280452818a7502d31a415403629baa502bd3 (patch) | |
| tree | bf563e01c37465a5adc46de917338631350c318c /dev/build | |
| parent | b8a71cf8281f85233e0b3d5568a85506157eb4d9 (diff) | |
| parent | 087e8c4c93c14de6038b79f4bbfd270124af2f11 (diff) | |
Merge PR #7344: Windows packaging build with Gitlab CI
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 f4ec218b6b..3608f7305d 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -970,6 +970,10 @@ function make_lablgtk { # These changes are included in dev/build/windows/patches_coq/lablgtk-2.18.3.patch log2 make world + + # lablgtk does not escape FINDLIBDIR path, which can contain backslashes + sed -i "s|^FINDLIBDIR=.*|FINDLIBDIR=$PREFIXOCAML/libocaml/site-lib|" config.make + log2 make install log2 make clean build_post |