main repositories on Github have been renamed

Last year Github changed the name for newly created repositories:

To align with this change we’ve decided to rename all our existing Github repositories.

If you run a local master branch of any of our repositories you need to update your local branch to main:

  1. $ git branch -m master main
  2. $ git fetch origin
  3. $ git branch -u origin/main main