Hacker News new | ask | show | jobs
by tadfisher 1389 days ago
From Git's perspective, the two "forks" share the same HEAD commit, e.g. they are merged. That is what a merge does. A branch is a name that exists independently of the commit and points to it, so the commit history is not actually a property of the branch, despite what Git UIs tell you.

Thus, in the underlying data structure behind the GitHub interface, there really isn't an "event" here to identify. The PR branch points to the same commit as the base branch, therefore both branches are in the state of existing as "merged" with one another.

So GitHub would have to track changes to the PR branch that result in this state separately from the existing "merge from GUI" and "push PR branch to master" changes, which I could imagine is fraught with edge cases that could result in what you consider a merge event ending up as a closed event.