Rename master branch to main

[thijskh]

As per the now Github defaults, I propose to move master branch to main. Github provides several helpful features to support this (redirects, shows contributors commands to update local copies, warns if you still push to master). Any objections?

[thijskh]

So no objections? I will then do it next week or so unless someone stops me.

[thijskh]

It has been done. Instructions to update local checkout are also on the front page of the repo but for completeness also here:

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