right - I tried it and git refused for the reason you guessed. It said: remote: error: By default, deleting the current branch is denied, because the next remote: error: 'git clone' won't result in any file checked out, causing confusion.
I followed Richard's advice, and pushed master: git push origin master and set up the tracking: git push origin -u master (from https://www.hostinger.com/tutorials/how-to-rename-a-git-branch/ ) I'll now request INFRA to set the default branch to master, so I can delete the old trunk. -Marshall On 9/17/2019 1:32 PM, Richard Eckart de Castilho wrote: > 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
