Change default branch to main

[calavera]

That's the default branch name that we've been using in all our repositories. I believe we should make the update here sooner rather than later.

[nmoutschen]

Sounds good!

I think the most important changes will be on the GitHub workflows (e.g. here), and we should keep the master branch for those that use it as a dependency, but we should definitively switch to main.

[calavera]

I've renamed the default branch already, run this to update your local repository:

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

GitHub redirects automatically from the old name to the new one, so using the repository as a dependency should still work.