Do not change PR from "needs work" to "needs review" after merge commit #40758
Description
Problem Description
The GitHub action responsible for managing labels on PRs changed the label to "needs review" after a commit. When a PR that is labelled "needs review" has a commit that just merges the develop branch this changes the status unnecessarily. Per discussion in https://groups.google.com/g/sage-devel/c/jTpHiM7YmTM, people find this clutters the list of PRs that actually need a review.
Proposed Solution
The action https://github.com/sagemath/sage/blob/develop/.github/sync_labels.py should not change "needs work" (maybe "needs info" too, but we don't use that as much so I'm not sure if it has different behaviour currently) to "needs review" when the commit message matches the default message for a merge commit.
Alternatives Considered
From the sage-devel discussion, there are good reasons to change "positive review" to "needs review", so that behaviour should remain. Authors should avoid merging develop after receiving a positive review unless they need to resolve merge conflicts (in which case another review is probably needed).
Additional Information
Merging develop should still trigger a new CI run. I don't imagine that this change would effect that though.
Check whether merging from the command line with git and merging from the GitHub web interface generate the same default merge commit messages.
Is there an existing issue for this?
- I have searched the existing issues for a bug report that matches the one I want to file, without success.