Rename 'master' git branch to 'main'

[julianhyde]

Rename the 'master' branch to 'main' in GitHub. 'Main' is the default name for new GitHub repositories, and over time 'master' will start to become an anachronism.

I have converted several repositories already, and the process is straightforward. It takes a 5 steps, and few seconds, for each client.

Here is the discussion thread.

[julianhyde]

Fixed in 36ab7b7.

To fix up a client, do the following:

git branch -m master main
git fetch origin
git branch -u origin/main main
git remote set-head origin -a