Rename default branch from master to main

[DavyLandman]

Let's rename the default branch for our repositories from master to main.

Github has tried to make this process as smooth as possible: https://github.com/github/renaming

Roughly, you rename the branch inside github, and it will take care of most redirecting, and will send the user a message about changed branch name during a push.

The following commands will be have to executed locally for every clone of a repo that has been renamed.

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

[jurgenvinju]

• rascal
• rascal-eclipse
• rascal-language-servers
• vallang
• rascal-maven-plugin
• capsule
• rascal-core
• typepal

[jurgenvinju]

will do the remaining projects after the Spring holiday; also when rascal-core has calmed down w.r.t. mvn configuration

[jurgenvinju]

• php-analysis

[mahills]

• php-analysis

Branch renamed.