Friendly reminder: Tag your submission
Written on 20.12.2020 22:19 by Michael Schwarz
Just a friendly reminder in case you have not tagged yet: the deadline is in approximately one and a half hours, so if you want your points, don't forget to tag! Also, ensure that your tag is pushed to the repository (git push --tags). If you see your tag in the git web interface, then it worked.