On 17. Sep 2019, at 18:13, Marshall Schor <[email protected]> wrote: > > I plan to do that, but will wait for an "OK" from Richard, in case there's an > issue which I don't know about :-).
Afaik one cannot rename remote branches, so you'll have to rename locally and then push under the new name. One of the branches is configured as the "default" branch in GitHub, currently "trunk". It is the branch which is shown when you go to the repo website with a browser. I don't know what happens if you try deleting that branch. Maybe GitHub prevents the deletion or maybe it selects another branch randomly to become the new "default" branch. To avoid any problems, I would suggest to: 1) rename trunk locally to master and push the new name 2) tell INFRA to protect master and to switch the default branch from "trunk" to "master" 3) delete trunk Cheers, -- Richard
