189cea9f80
This PR adds a CI check that fails when a PR introduces no changes compared to its base branch. This catches cases where a duplicate PR is queued for merge after an identical PR has already landed (as happened with https://github.com/leanprover/lean4/pull/12876 and https://github.com/leanprover/lean4/pull/12877). The check is added as a second job in the existing `check-stage0.yml` workflow, which already has the same trigger conditions and git setup pattern. On `pull_request` events it diffs against the merge base; on `merge_group` events it diffs `HEAD^1..HEAD` (the PR's contribution to the synthetic merge commit). Note that batched merge groups are treated as a unit — if the entire group is non-empty the check passes, which is the right behaviour for lean4's typical single-PR queuing. 🤖 Prepared with Claude Code Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
29 lines
867 B
YAML
29 lines
867 B
YAML
name: Check for empty PR
|
|
|
|
on:
|
|
merge_group:
|
|
pull_request:
|
|
|
|
jobs:
|
|
check-empty-pr:
|
|
runs-on: ubuntu-latest
|
|
steps:
|
|
- uses: actions/checkout@v6
|
|
with:
|
|
ref: ${{ github.event_name == 'pull_request' && github.event.pull_request.head.sha || github.sha }}
|
|
fetch-depth: 0
|
|
filter: tree:0
|
|
|
|
- name: Check for empty diff
|
|
run: |
|
|
if [[ "${{ github.event_name }}" == "pull_request" ]]; then
|
|
base=$(git merge-base "origin/${{ github.base_ref }}" HEAD)
|
|
else
|
|
base=$(git rev-parse HEAD^1)
|
|
fi
|
|
if git diff --quiet "$base" HEAD --; then
|
|
echo "This PR introduces no changes compared to its base branch." | tee "$GITHUB_STEP_SUMMARY"
|
|
echo "It may be a duplicate of an already-merged PR." | tee -a "$GITHUB_STEP_SUMMARY"
|
|
exit 1
|
|
fi
|
|
shell: bash
|