diff options
| author | Théo Zimmermann | 2020-12-18 13:13:10 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-12-18 13:13:10 +0100 |
| commit | c99cf105cc62b640b8b6cc97ad85bdca59aa84fe (patch) | |
| tree | 091a8795e118b83aac73352869b61a6bd280fcab /dev/build | |
| parent | e11d3f6d5a5045f38f0a17fb15e9674c714d372f (diff) | |
Do not load overlay data (workaround to fix CI).
Diffstat (limited to 'dev/build')
| -rwxr-xr-x | 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 6b59c987fb..beed8bc443 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1435,12 +1435,12 @@ function make_coq { # make clean # Copy these files somewhere the plugin builds can find them - logn copy-basic-overlays cp dev/ci/ci-basic-overlay.sh /build/ + #logn copy-basic-overlays cp dev/ci/ci-basic-overlay.sh /build/ build_post fi - load_overlay_data + #load_overlay_data } ##### GNU Make for MinGW ##### |