"Automatically delete the branch right after merging a PR, if possible" should be optional

[jimklimov]

After installing the browser plugin, the GitHub Web-GUI no longer offers a checkbox to delete original branches of PRs but just kills them off (and then I can "Undo" the action). For many workflows it makes sense, however for some of ours it does not. Can this feature be changed to showing the checkbox like original GitHub does, just perhaps pre-ticking it to keep Refined GitHub's default behavior expected by its long-time users?

I got a bit lost in the long list of options I can configure for the extension in my browser, so not sure if there is a setting for this behavior already, or if the branch deletion is currently hardcoded.

Thanks a lot for the nifty extension :)

[jimklimov]

Upon some more poring into the extension options, there is a "pr-branch-auto-delete" toggle so at least that is configurable (at least a reference from README about the feature is an easy fix that would help those in my shoes).

[fregante]

It’s optional and it is in the (admittedly very long) readme:

Automatically deletes the branch right after merging a PR, if possible.

In both the readme and the settings page, you can filter/search “delete” to find it easily.

If your workflow expects long-lived branches, then they should be protected in the native repo settings itself.