fix· GitHub
Warnings for commits pushed after merge
Follow-up commits left out of a merged PR now get a recovery warning.
A PR can merge while an agent is still working on a follow-up. We now report the branch and pushed commit that missed that merge, so you can open a follow-up PR instead of assuming the changes reached the base branch.
The check also handles squash merges. We do not open another PR automatically, and an unchanged or deleted branch does not produce a missing-commit warning.
#1518