Stream: Coq devs & plugin devs

Topic: GitLab mirroring


view this post on Zulip Théo Zimmermann (Jun 02 2022 at 09:02):

@Gaëtan Gilbert Have you been trying to fix the GitLab mirroring at the same time as me?

view this post on Zulip Gaëtan Gilbert (Jun 02 2022 at 09:04):

maybe

view this post on Zulip Théo Zimmermann (Jun 02 2022 at 09:06):

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: Jun 04 2023 at 19:30 UTC