chore: prevent stage0 updates from being merged using the merge queue

.github/workflows/check-prelude.yml

@@ -1,26 +1,21 @@
-name: Check for modules that should use `prelude`
+name: Check for copyright header
 
-on: [pull_request]
+on: [merge_group]
 
 jobs:
-  check-prelude:
+  check-lean-files:
     runs-on: ubuntu-latest
     steps:
-      - name: Checkout
-        uses: actions/checkout@v4
-        with:
-          # the default is to use a virtual merge commit between the PR and master: just use the PR
-          ref: ${{ github.event.pull_request.head.sha }}
-          sparse-checkout: src/Lean
-      - name: Check Prelude
-        run: |
-          failed_files=""
-          while IFS= read -r -d '' file; do
-            if ! grep -q "^prelude$" "$file"; then
-              failed_files="$failed_files$file\n"
-            fi
-          done < <(find src/Lean -name '*.lean' -print0)
-          if [ -n "$failed_files" ]; then
-            echo -e "The following files should use 'prelude':\n$failed_files"
-            exit 1
-          fi
+    - uses: actions/checkout@v4
+      with:
+        ref: ${{ github.event.pull_request.head.sha }}
+    - name:
+      run: |
+        if git diff HEAD^..HEAD --name-only -- stage0 |
+           grep -v -x -F stage0/src/stdlib_flags.h |
+           grep -v -x -F stage0/src/lean.mk.in |
+           grep -q .
+        then
+          echo "Found stage0 updates, please do not merge using the merge queue" | tee "$GITHUB_STEP_SUMMARY"
+          exit 1
+        fi