@Gaëtan Gilbert Have you been trying to fix the GitLab mirroring at the same time as me?
maybe
So just FTR, I don't know what the initial problem was but a few days ago, I tried to solve it by removing and resetting the mirroring. This worked once, but then failed to update again. What I had forgotten about was that we restrict who can push to protected branches on GitLab to just coqbot. So today, I've logged into the coqbot GitLab account to reset the mirroring using this account. It looks like it worked now.
Last updated: Oct 13 2024 at 01:02 UTC