aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMichael Soegtrop2020-11-18 22:00:43 +0100
committerMichael Soegtrop2020-11-18 22:00:43 +0100
commitfea83b040f285e4316fd9d63d4c940d9fe444d91 (patch)
tree8736c1e582c05846ed3604f5101ee90d5d2a9578 /dev
parente2f2966c453ecdf788ee1c15d62be68da2cddebe (diff)
parentc02301699e9014862c52f069a130b8131fd9d692 (diff)
Merge PR #13389: [ci/gitlab/windows] Do not load user overlays.
Reviewed-by: MSoegtropIMC
Diffstat (limited to 'dev')
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh9
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