diff options
| -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 |