ci: Fix workflow launch on matrix-unrelated labels (#7812)

.github/workflows/on-pr.yml

@@ -25,18 +25,11 @@ on:
       - unlabeled
 
 concurrency:
-  # Use a per-ref group so a newer run (a push, or a change to a label below)
-  # supersedes the in-progress one for that ref. Label events we don't act on get
-  # their own unique group (per run id) instead, keeping them out of the shared
-  # group so real builds keep running. Keep this list in sync with `should-run`.
-  group: >-
-    ${{ github.workflow }}-${{ github.ref }}${{
-      ((github.event.action == 'labeled' || github.event.action == 'unlabeled')
-      && github.event.label.name != 'Ready to merge'
-      && github.event.label.name != 'DraftRunCI'
-      && github.event.label.name != 'Full CI build')
-      && format('-{0}', github.run_id) || ''
-    }}
+  # A single per-ref group with cancel-in-progress means any newer run (a push
+  # or a label change) supersedes the in-progress one for that ref. Keeping
+  # exactly one authoritative run per ref ensures a fast do-nothing run can never
+  # mask a real build's checks.
+  group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 defaults:
@@ -44,21 +37,17 @@ defaults:
     shell: bash
 
 jobs:
-  # This job determines whether the rest of the workflow should run. It runs
-  # when the PR is not a draft (which should also cover merge-group) or has the
-  # 'DraftRunCI' or 'Full CI build' label. For label events it only runs when the
-  # label added or removed is one we act on ('Ready to merge', 'DraftRunCI' or
-  # 'Full CI build'), so unrelated label changes do not trigger a redundant run.
+  # This job determines whether the rest of the workflow should run at all,
+  # based on the current set of labels: it runs when the PR is not a draft
+  # (which should also cover merge-group) or has the 'DraftRunCI' or
+  # 'Full CI build' label. Whether a build then happens, and whether it is the
+  # minimal or full matrix, is decided further below and in the strategy matrix.
   should-run:
     if: >-
       ${{
-        ((github.event.action != 'labeled' && github.event.action != 'unlabeled')
-          || github.event.label.name == 'Ready to merge'
-          || github.event.label.name == 'DraftRunCI'
-          || github.event.label.name == 'Full CI build')
-        && (!github.event.pull_request.draft
-          || contains(github.event.pull_request.labels.*.name, 'DraftRunCI')
-          || contains(github.event.pull_request.labels.*.name, 'Full CI build'))
+        !github.event.pull_request.draft
+        || contains(github.event.pull_request.labels.*.name, 'DraftRunCI')
+        || contains(github.event.pull_request.labels.*.name, 'Full CI build')
       }}
     runs-on: ubuntu-latest
     steps: