Closed DmxLarchey closed 6 years ago
I have no objections. You should do this in the following way on your local file system: git checkout correctionforCoq881
(make also sure it is up to date) then git branch -b master
then use the settings of your Github repo to set the current branch to master (again), then you can delete correctionforCoq881. Thus instead of renaming, this copies pointers, adjusts the global settings and then cleans up.
What is the -b for in the command git branch -b master
I cannot find it in the doc ?
Ok the command was git checkout -b master
and then git push --set-upstream origin master
and after that I changed the default branch in GH. For the moment I do not erase correctionforCoq881
until we both have switched to master as default. I close the issue.
The default branch is currently correctionforCoq881 and I would like to rename it to master. I deleted master which was dead for a long time anyway and contained in correctionforCoq881 so the branch name 'master' is free for use.
Do agree to do that ? Would it pose a technical pb for you ?