diff options
author | Junio C Hamano <gitster@pobox.com> | 2023-11-02 10:53:15 +0300 |
---|---|---|
committer | Junio C Hamano <gitster@pobox.com> | 2023-11-02 10:53:15 +0300 |
commit | ec7cc187d48e5d23d5eebd273ce62d2b7aaa8e4f (patch) | |
tree | 9a44856604a0b254aa05e2f2ccf8d52065312b21 /.github/workflows/main.yml | |
parent | 50758312f2d29a32858ccd25b24ea64ae8a04cb1 (diff) | |
parent | 99fe06cbfd660726b1601a4d36897ed90e5d5b64 (diff) |
Merge branch 'jc/ci-skip-same-commit' into maint-2.42
Tweak GitHub Actions CI so that pushing the same commit to multiple
branch tips at the same time will not waste building and testing
the same thing twice.
* jc/ci-skip-same-commit:
ci: avoid building from the same commit in parallel
Diffstat (limited to '.github/workflows/main.yml')
-rw-r--r-- | .github/workflows/main.yml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 079645b776..1b41278a7f 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -5,6 +5,19 @@ on: [push, pull_request] env: DEVELOPER: 1 +# If more than one workflow run is triggered for the very same commit hash +# (which happens when multiple branches pointing to the same commit), only +# the first one is allowed to run, the second will be kept in the "queued" +# state. This allows a successful completion of the first run to be reused +# in the second run via the `skip-if-redundant` logic in the `config` job. +# +# The only caveat is that if a workflow run is triggered for the same commit +# hash that another run is already being held, that latter run will be +# canceled. For more details about the `concurrency` attribute, see: +# https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#concurrency +concurrency: + group: ${{ github.sha }} + jobs: ci-config: name: config |