ci: cancel stale pull request workflow runs

The CI workflow groups all runs by commit hash using
`group: ${{ github.sha }}`.  This means every push to a pull
request starts a separate workflow run, and all workflows
triggered by the same commit share the same concurrency group.

With this change, pull request runs are grouped by pull request
number instead of commit hash, and runs superseded by a newer
push are canceled.  The concurrency group becomes
`${{ github.workflow }}-${{ github.event.pull_request.number ||
github.sha }}` and `cancel-in-progress` is set to true for
pull request events.

For pull request events, the group is `<workflow>-<pull-request-number>`
(e.g., "main-workflow-42").  If you push a new commit to an
existing pull request before the CI working on it finishes, the
new request will be placed in the same group and cancel the
currently running run.

For non-pull-request events, the group is `${{ github.workflow }}-${{
github.sha }}` and `cancel-in-progress` defaults to false, so
there is no regression in behavior.

Note that the previous configuration used `group: ${{ github.sha }}`,
which meant all workflows sharing the same commit hash were in the
same group.  The new configuration includes the workflow name in
the group, so each workflow has its own concurrency group per
commit/PR.

Signed-off-by: Harald Nordgren <haraldnordgren@gmail.com>
Signed-off-by: Junio C Hamano <gitster@pobox.com>

0 files changed, 0 insertions, 0 deletions