I pushed the branch but I guess I am not an admin so cannot make this change to the GH settings. I will re-target my open PRs now, but someone will need to change the default.
Also, I re-targeted active existing PRs to main. So once we change the primary branch it should just be a matter of moving the last few (and any which open in the mean time against master) and then contributors switching in their local copies.
I鈥檝e changed the setting.
If you delete the master branch, URLs will redirect properly.
Is there any tool that does all the things that need to be done (add new branch, change all open PRs, change settings, delete old branch, etc) in one go?
I believe there is, I can't remember what it was called though. In this case there was so little work I just did it manually. For more active repos it would be awesome to automate.
Eventually github will support doing all those things natively and automatically; in general my suggestion is for repos to immediately start new with "main", but to consider holding off on the switch until github's finished shipping the features for it.
Branch removed and comments made on the closed PRs if folks want to take them up again.