diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-09 13:11:29 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-16 16:27:07 +0100 |
| commit | 0be785a5832177efa4ec396a421a4eb367b81914 (patch) | |
| tree | 46f1873a92108c02f73a84233a0e6018f949e092 /dev/ci/ci-common.sh | |
| parent | dfe41b6a564203c12a2fc2618f3082f971225022 (diff) | |
Source basic overlay before user overlays.
Diffstat (limited to 'dev/ci/ci-common.sh')
| -rw-r--r-- | dev/ci/ci-common.sh | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 676edb740..1838db5d0 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -28,10 +28,12 @@ ls "$COQBIN" # Where we clone and build external developments CI_BUILD_DIR="$PWD/_build_ci" +# shellcheck source=ci-basic-overlay.sh +source "${ci_dir}/ci-basic-overlay.sh" for overlay in "${ci_dir}"/user-overlays/*.sh; do - source "${overlay}" + # shellcheck source=/dev/null + source "${overlay}" done -source "${ci_dir}/ci-basic-overlay.sh" mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" |