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"
... View more