Move CI-only check-diff script to .github/

.github/workflows/check-diff.yml

@@ -0,0 +1,27 @@
+name: Diff completeness check
+on: pull_request
+
+env:
+  # Force colored output (see https://bixense.com/clicolors/ and https://force-color.org/)
+  TERM: xterm-256color
+  CLICOLOR: 1
+  CLICOLOR_FORCE: 1
+
+jobs:
+  check-diff:
+    runs-on: ubuntu-slim
+    steps:
+      - name: Clone repo
+        uses: actions/checkout@v7
+        with:
+          ref: ${{ github.event.pull_request.head.sha }}
+      - name: Check diff
+        shell: bash # Bash is the default, but specifying it explicitly enables `-o pipefail`.
+        run: |
+          MERGE_BASE=$(gh api "/repos/{owner}/{repo}/compare/$BASE_SHA...$HEAD_SHA" --jq '.merge_base_commit.sha')
+          git fetch origin "$MERGE_BASE"
+          .github/scripts/check-diff.bash "$MERGE_BASE" | sed -E 's/^/::warning::/'
+        env:
+          BASE_SHA: ${{ github.event.pull_request.base.sha }}
+          HEAD_SHA: ${{ github.event.pull_request.head.sha }}
+          GH_TOKEN: ${{ github.token }}