Closed desruisseaux closed 3 years ago
Sounds good to me
Having hear no objection in one week, I will proceed.
Apparently I do not have administrator right for doing this operation. If someone with more power is willing to do the renaming, it should take only one minute (click on the pen on the right side of "master" on this page).
@desruisseaux you've now got admin rights to this repository. Please fix it yourself and remember that with great power comes great responsibility :-)
Thanks, renaming applied. Local clones can update as below (copied from GitHub instructions):
git branch -m master main
git fetch origin
git branch -u origin/main main
git remote set-head origin -a
Should we rename the
master
branch hasmain
? The procedure is described here and seems simple: