[masklinn]

It's the latter.

Basically, aside from github's merge button (which does magic inaccessible to mere mortal[0]) the signal github looks for to know whether a PR is merged is whether the PR's head commit is in the target branch.

So if you reset the PR's branch to the target (or any of its commit), as far as github is concerned it's as if the PR had been merged.

[0] the ability to close PRs as merged was requested 3 years ago on the old discourse forum, which was deleted when github deployed the new community thingie, the request was reposted on the new site https://github.com/community/community/discussions/12437

[sighingnow]

+1 for the feature of marking as merged, as in many projects, e.g., apache arrow, the pull requests are merged in a different way and all pull requests are showed as "closed" rather than "merged".

It would cause some confusion for project management, I guess.