Extract the PR build gate into a reusable workflow

The gate job was copy-pasted into build-ilspy.yml and build-frontends.yml
and the two copies had already started drifting (job casing, comment
wording). A workflow_call workflow keeps a single definition; the callers
shrink to a uses: job and route its "run" output to their build jobs
unchanged. Each caller must still grant pull-requests: read explicitly,
because the called workflow's token is the intersection of what the
caller grants and what the callee requests, and both callers default to
contents: read only.

Assisted-by: Claude:claude-fable-5:Claude Code

.github/workflows/build-frontends.yml

@@ -10,27 +10,11 @@ permissions:
   contents: read
 
 jobs:
-  # Skip push builds for branches whose open PR (base master/release/*) already builds
-  # them via the pull_request trigger. Pushes to master/release/* always build.
+  # Skip push builds for branches whose open PR already builds them; see pr-build-gate.yml.
   gate:
-    runs-on: ubuntu-latest
     permissions:
       pull-requests: read
-    outputs:
-      run: ${{ steps.check.outputs.run }}
-    steps:
-    - id: check
-      env:
-        GH_TOKEN: ${{ github.token }}
-      run: |
-        prs=0
-        case "$GITHUB_EVENT_NAME/$GITHUB_REF_NAME" in
-          push/master|push/release/*) ;;
-          push/*) prs=$(gh api -X GET "repos/$GITHUB_REPOSITORY/pulls" -f state=open \
-            -f head="$GITHUB_REPOSITORY_OWNER:$GITHUB_REF_NAME" \
-            --jq 'map(select(.base.ref == "master" or (.base.ref | startswith("release/")))) | length') ;;
-        esac
-        echo "run=$([ "$prs" = 0 ] && echo true || echo false)" >> "$GITHUB_OUTPUT"
+    uses: ./.github/workflows/pr-build-gate.yml
 
   build:
     needs: gate

.github/workflows/build-ilspy.yml

@@ -15,27 +15,11 @@ env:
   StagingDirectory: buildartifacts
 
 jobs:
-  # Skip push builds for branches whose open PR (base master/release/*) already builds
-  # them via the pull_request trigger. Pushes to master/release/* always build (they publish).
+  # Skip push builds for branches whose open PR already builds them; see pr-build-gate.yml.
   Gate:
-    runs-on: ubuntu-latest
     permissions:
       pull-requests: read
-    outputs:
-      run: ${{ steps.check.outputs.run }}
-    steps:
-    - id: check
-      env:
-        GH_TOKEN: ${{ github.token }}
-      run: |
-        prs=0
-        case "$GITHUB_EVENT_NAME/$GITHUB_REF_NAME" in
-          push/master|push/release/*) ;;
-          push/*) prs=$(gh api -X GET "repos/$GITHUB_REPOSITORY/pulls" -f state=open \
-            -f head="$GITHUB_REPOSITORY_OWNER:$GITHUB_REF_NAME" \
-            --jq 'map(select(.base.ref == "master" or (.base.ref | startswith("release/")))) | length') ;;
-        esac
-        echo "run=$([ "$prs" = 0 ] && echo true || echo false)" >> "$GITHUB_OUTPUT"
+    uses: ./.github/workflows/pr-build-gate.yml
 
   Build:
     name: Desktop (Windows)

.github/workflows/pr-build-gate.yml

@@ -0,0 +1,32 @@
+name: PR build gate
+
+on:
+  workflow_call:
+    outputs:
+      run:
+        description: Whether the push-triggered build should run
+        value: ${{ jobs.gate.outputs.run }}
+
+jobs:
+  # Skip push builds for branches whose open PR (base master/release/*) already builds
+  # them via the pull_request trigger. Pushes to master/release/* always build (they
+  # may publish packages, and no PR of theirs may suppress that).
+  gate:
+    runs-on: ubuntu-latest
+    permissions:
+      pull-requests: read
+    outputs:
+      run: ${{ steps.check.outputs.run }}
+    steps:
+    - id: check
+      env:
+        GH_TOKEN: ${{ github.token }}
+      run: |
+        prs=0
+        case "$GITHUB_EVENT_NAME/$GITHUB_REF_NAME" in
+          push/master|push/release/*) ;;
+          push/*) prs=$(gh api -X GET "repos/$GITHUB_REPOSITORY/pulls" -f state=open \
+            -f head="$GITHUB_REPOSITORY_OWNER:$GITHUB_REF_NAME" \
+            --jq 'map(select(.base.ref == "master" or (.base.ref | startswith("release/")))) | length') ;;
+        esac
+        echo "run=$([ "$prs" = 0 ] && echo true || echo false)" >> "$GITHUB_OUTPUT"