Automatically set delete_branch_on_merge for repositories

[Kobzol]

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.

[ehuss]

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?

[Kobzol]

My understanding is that this only deletes the source branch after a PR is merged.

[ehuss]

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?

[Kobzol]

Do we ever create PRs out of the auto branch? 🤔

Anyway, good questions, I will try to find out.

[Kobzol]

GitHub claims that the head (source) branch of a PR will be removed after a merge.

I did a few experiments:

• Merge a PR through GH API: the head branch is deleted.
• Merge a branch directly into main: the merged branch is not deleted.
• Merge a branch directly into main, when a PR is opened from that branch: the head branch is deleted.
• Merge a branch directly into 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.

[rylev]

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?

[Kobzol]

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.