Hi all,
We have updated the domjudge git repository to rename the master branch to
main. Please update any local checkouts by running:
git branch -m master main
git fetch origin
git branch -u origin/main main
git remote set-head origin -a
Regards,
Thijs Kinkhorst
on behalf of the DOMjudge team
