diff options
| author | Michael Soegtrop | 2020-11-18 22:00:43 +0100 |
|---|---|---|
| committer | Michael Soegtrop | 2020-11-18 22:00:43 +0100 |
| commit | fea83b040f285e4316fd9d63d4c940d9fe444d91 (patch) | |
| tree | 8736c1e582c05846ed3604f5101ee90d5d2a9578 /dev | |
| parent | e2f2966c453ecdf788ee1c15d62be68da2cddebe (diff) | |
| parent | c02301699e9014862c52f069a130b8131fd9d692 (diff) | |
Merge PR #13389: [ci/gitlab/windows] Do not load user overlays.
Reviewed-by: MSoegtropIMC
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 |
