Cancel in-progress jobs on updated push

At times, PRs can go through multiple pushes in a short amount of time,
spawning a workflow run for each. Most of the time, there's no need to
let the previous jobs running if the code itself has changed (e.g., via
a force push), and we'd benefit from having those slots be used by other
PRs/branches instead.

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index b00bf47fe66100fa8ad9ffbd2a981ff419528eb7..8e02ec9da75c803caa0dfd9b797ea6b892a13298 100644 (file)
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -8,6 +8,10 @@ on:
     branches-ignore:
       - master
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   build:
     strategy: