14 Jul
2021
14 Jul
'21
3:14 a.m.
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