Description
In the wake of recent events, a good part of the git-using community is converging to use main as the name for the default branch instead of master. Some related discussion:
https://twitter.com/mislav/status/1270388510684598272?s=21
https://mail.gnome.org/archives/desktop-devel-list/2019-May/msg00066.html
And github seems to be changing the default branch to main: https://twitter.com/natfriedman/status/1271253144442253312
Right now on our repo we have:
$ git grep master | wc
122 771 13973and most of them are references to our master branch.
This issue is for us to talk about whether or not we want to change the name of the default branch, and if yes, to what, and how.
I'm personally in favor of main, but I also understand the implications of all the scripts out there which rely on the name of the main branch. So I'd propose creating a new main branch, changing the default branch in github to main, but not delete the master branch for a good while, and have a part of the CI keep rebasing deprecated master with main.