diff options
| -rw-r--r-- | src/ci/github-actions/jobs.yml | 4 | ||||
| -rwxr-xr-x | src/ci/scripts/checkout-submodules.sh | 4 |
2 files changed, 8 insertions, 0 deletions
diff --git a/src/ci/github-actions/jobs.yml b/src/ci/github-actions/jobs.yml index 3f8ea696ee2..43c77d1ddf7 100644 --- a/src/ci/github-actions/jobs.yml +++ b/src/ci/github-actions/jobs.yml @@ -129,6 +129,10 @@ pr: - name: mingw-check-tidy continue_on_error: true free_disk: false + env: + # This submodule is expensive to checkout, and it should not be needed for + # tidy. This speeds up the PR CI job by ~1 minute. + SKIP_SUBMODULES: src/gcc <<: *job-linux-4c - name: x86_64-gnu-llvm-19 env: diff --git a/src/ci/scripts/checkout-submodules.sh b/src/ci/scripts/checkout-submodules.sh index 5bb343241ae..3b646587dc2 100755 --- a/src/ci/scripts/checkout-submodules.sh +++ b/src/ci/scripts/checkout-submodules.sh @@ -55,7 +55,11 @@ for i in ${!modules[@]}; do bg_pids[${i}]=$! continue else + # Submodule paths contained in SKIP_SUBMODULES (comma-separated list) will not be + # checked out. + if [ -z "${SKIP_SUBMODULES:-}" ] || [[ ! ",$SKIP_SUBMODULES," = *",$module,"* ]]; then use_git="$use_git $module" + fi fi done retry sh -c "git submodule deinit -f $use_git && \ |