diff options
| author | Théo Zimmermann | 2020-11-15 15:35:43 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-15 15:35:43 +0100 |
| commit | c02301699e9014862c52f069a130b8131fd9d692 (patch) | |
| tree | f9cba092257b65fff6c53203b0ca49fe476e865f /dev | |
| parent | 9a93f5836a5f7bab81384314ac11ff0aac7d1b7f (diff) | |
[ci/gitlab/windows] Do not load user overlays.
This was broken since #13177. We remove support for user overlays in
Windows build instead of fixing it since there is no specific use
case.
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index fc8921e63d..6f6b3cd6d2 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -404,8 +404,7 @@ function build_prep { # ------------------------------------------------------------------------------ # Like build_prep, but gets the data from an entry in ci-basic-overlay.sh -# This assumes the following definitions exist in ci-basic-overlay.sh, -# or in a file in the user-overlays folder: +# This assumes the following definitions exist in ci-basic-overlay.sh # $1_CI_REF # $1_CI_ARCHIVEURL # $1_CI_GITURL @@ -432,7 +431,7 @@ function build_prep_overlay { } # ------------------------------------------------------------------------------ -# Load overlay version variables from ci-basic-overlay.sh and user-overlays/*.sh +# Load overlay version variables from ci-basic-overlay.sh # ------------------------------------------------------------------------------ function load_overlay_data { @@ -448,9 +447,6 @@ function load_overlay_data { export CI_PULL_REQUEST="" fi - for overlay in /build/user-overlays/*.sh; do - . "$overlay" - done . /build/ci-basic-overlay.sh } @@ -1441,7 +1437,6 @@ function make_coq { # Copy these files somewhere the plugin builds can find them logn copy-basic-overlays cp dev/ci/ci-basic-overlay.sh /build/ - logn copy-user-overlays cp -r dev/ci/user-overlays /build/ build_post fi |
