ci: let a push to main cancel the build of the previous one

Push builds of main ran one after another, so a merge waited for the
builds of every earlier merge before main got a result for its tree; a
fix of a red main sat behind a build of the tree it fixes. The newest
push now cancels the build in progress, like pull request and dispatched
builds already do. The merge queue's baselines already skip cancelled
main builds and use the nearest completed ones.

Co-Authored-By: Claude <noreply@anthropic.com>
This commit is contained in:
Adrià FranchandClaude committed 2026-10-16 19:14:07 +02:00
1 parent 66e290f1c0
commit bca62ea696
1 file changed
+1 -1
+1 -1
View File
@@ -28,7 +28,7 @@ permissions:
concurrency:
group: build-${{ github.event_name }}-${{ github.event.pull_request.number || inputs.pr || github.ref }}
cancel-in-progress: ${{ github.event_name != 'push' }}
cancel-in-progress: true
env:
CONFIGURE: >-