Oh btw with all these cherry picks on

origin

, I think the default currently isn't to clean up branches on merge. Should we enable that?

Automatically delete head branches

We shouldn't have merge branches on origin, right?

🤷‍♂️ It's certainly easier, and expected from the GHA perspective

If we have a consistent naming scheme and

origin

only has “managed” branches (main, releases, automation), it’s probably okay? I know it’s easy for humans to accidentally push to it, though

We shouldn't have merge branches on origin, right?

This still doesn't answer the question 🙂

Well, I'm trying to understand why this would be necessary, i.e., what would be deleted?

It would only delete the PRs branch, right. So wether we have other branches pushed or not doesn’t apply, iiuc. +1 to auto delete.

The PR source branch is on a fork though, right?

Not always, and my original ccomment was that I'm not sure if this applies to forks or not. i suspect no. The branches pushed to

origin

I've seen are: • Branches from our GitHub Actions. That's pretty standard since

GITHUB_TOKEN

is widely used • Branches created using the web UI for editing a file, and the editor has permissions to push to

origin

. (Such as myself) ◦ Normally GitHub pushes to a branch, but that isn't an option if you can push to

origin

. I've made at least a dozen of these PRs. They are exceedingly easy to do for fixing typos/nits/.etc...

Nope, I just wanted to understand why

🚀