Open Kobzol opened 7 months ago
Will this delete things like auto
branches? It seems somewhat dangerous to turn this on for everyone, since we don't know if there are repos with long-lived branches. I'm not really clear when this does and does not delete branches. Does it only delete if merged directly from a PR?
My understanding is that this only deletes the source branch after a PR is merged.
But what if the source branch is auto
? Won't that delete it? How does it determine what a "source branch" is? Does it have to be the branch that is on a PR itself? Does deleting happen for merges not done through the GitHub UI? What about merges done through the GitHub API?
Do we ever create PRs out of the auto
branch? :thinking:
Anyway, good questions, I will try to find out.
GitHub claims that the head (source) branch of a PR will be removed after a merge.
I did a few experiments:
main
: the merged branch is not deleted.main
, when a PR is opened from that branch: the head branch is deleted.main
, where a PR is opened from a branch auto
that has the same commit SHA: the head branch is deleted, auto
is not deleted.So it seems that the logic looks like this: if a PR is opened from branch b
, and that PR is marked as merged (by any means, be it UI, GH API, or the head commit of b
appearing in main
/master
), then b
will be deleted.
This makes me nervous since there are situations where this is a destructive action (e.g., when squashing on merge).
Does this work the same way for forks of a repo or is this only happening when the branch is in the same repo as the branch being merged into?
Does this work the same way for forks of a repo or is this only happening when the branch is in the same repo as the branch being merged into?
It doesn't delete the branches from forks.
This was requested for the
miri-test-libstd
repository, but I think that it's generally useful to set this everywhere, which this PR does.