usethesource / usethesource.github.io

Organization website for UseTheSource
1 stars 2 forks source link

Rename default branch from master to main #18

Open DavyLandman opened 3 years ago

DavyLandman commented 3 years ago

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 commented 2 years ago
jurgenvinju commented 2 years ago

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

jurgenvinju commented 1 year ago
mahills commented 1 year ago
  • [x] php-analysis

Branch renamed.