Le mardi 06 octobre 2020 à 17:11 +0200, Michael Scherer a écrit :
> I am looking at the current gerrit issue (cant push), I may restart
> gerrit around to do some maintainance. I will send a email once
It should be back.
Problem was likely some git process that crashed and left a lock file.
Given the migration to github is soon, I am not going to investigate
much on that and see why it crashed :)
Michael Scherer / He/Il/Er/Él
Sysadmin, Community Infrastructure