The "Merge Button" API allows marking a PR as merged even if the PR's actual commits don't end up in the target branch (e.g. "squash" or "rebase" merges).
However, when closing PRs via the PR API it's not possible to override the "merged" flag (github sets it automatically based on the PR head landing in the target branch, or so I guess). So in situations where a tool wants to perform PR integration itself (such as the implementing not rocket science rule of software engineering), it becomes impossible to mark PRs as "merged" in the github sense, it's only possible to use ad-hoc flags to try and differentiate "closed and integrated" from "closed and rejected".
Would it be possible to add the ability to set / override the merged status in the PR API, something the Merge Button API can apparently do internally?
Request context: people would like bors-ng to provide more integration strategies than just a merge commit, currently this requires picking the least bad option between "don't integrate the actual commits we tested" and "lose the merged flag"
I support this idea. There are a variety of merge bots that integrate with GitHub. These apps should be able to mark a pull request as "Merged" so that it gets the purple "Merged" badge.
Thank you for your feedback! We're always working to improve GitHub and the GitHub Community Forum, and we consider every suggestion we receive. I've logged your feature request in our internal feature request list.
Though I can't guarantee anything or share a timeline for this, I can tell you that it's been shared with the appropriate teams for consideration.
Once again, thank you for your input!
Mark helpful posts with Accept as Solution to help other users locate important info. Don't forget to give Kudos for great content!
I would find this feature very useful. I use GitHub Enterprise so I would very much like it to be available there as well.