Merge branch 'jc/ci-skip-same-commit'

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

Author: gitster

.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