[masklinn]

> That's pretty much the Github logic.

Of note: github can actually override this logic internally, in a way which they have not made accessible through the API: if you use github's merge button to squash or rebase-merge a PR, it'll be marked as merged, despite the PR's commits not being part of the target branch.

[eslaught]

I think the current behavior is useful: if the repo owner decides to merge a PR manually (e.g., with the git command line), the PR ends up in a merged state as expected. Otherwise the owner has to do two actions: first on the command line, and then (to avoid duplicate merge commits) close (not merge!) on the web interface. Beyond the extra work, it's ugly because all the PRs in the repo are (incorrectly) marked as closed, not merged.

The issue seems to be that there is no provenance tracking. If a commit appears first in the contributed repo, and then makes its way into the base branch, I think that can reasonably be considered merged; if the contributed branch gets overwritten with commits already in the base branch, that is no longer a contribution at all and just the contributor resetting the branch (perhaps with malicious intent, or else through sheer ignorance).

[junon]

I mean, yeah. This isn't the only status logic. Just one part I've observed. GitHub is very much event-based.