Comment by fen4o

Tried to do a git push - it succeeded after 3 mins. Then I wanted to open a PR and it failed with a 500 error.

Facepalmed and decided that this is it for today.