diff options
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 2 | ||||
| -rw-r--r-- | dev/ci/ci-common.sh | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 60108cda4f..8a49b97dac 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1448,10 +1448,10 @@ function make_addons { export CI_BRANCH="" export CI_PULL_REQUEST="" fi - . /build/ci-basic-overlay.sh for overlay in /build/user-overlays/*.sh; do . "$overlay" done + . /build/ci-basic-overlay.sh for addon in $COQ_ADDONS; do "make_addon_$addon" diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 3536cc70b2..7af648f0a6 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -37,12 +37,12 @@ ls "$COQBIN" # Where we download and build external developments CI_BUILD_DIR="$PWD/_build_ci" -# shellcheck source=ci-basic-overlay.sh -. "${ci_dir}/ci-basic-overlay.sh" for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null . "${overlay}" done +# shellcheck source=ci-basic-overlay.sh +. "${ci_dir}/ci-basic-overlay.sh" # [git_download project] will download [project] and unpack it # in [$CI_BUILD_DIR/project] if the folder does not exist already; |