Stern inaktivStern inaktivStern inaktivStern inaktivStern inaktiv
 

I just became aware github decided to use main as the default branch instead of master for any new created repositories. That's why I decided to rename all my default branches from master to main on github.

I also had to update my local clones to use main instead of master and wrote a tiny script to achieve this. Just download this script and execute it in the cloned directory.