Stream: coq-community devs & users

Topic: GitLab mirroring issues


view this post on Zulip Karl Palmskog (Jul 27 2020 at 08:15):

I noticed that stalmarck is not being mirrored at GitLab anymore (maybe due to some force-push). There are also maybe 5-6 new projects that are not mirrored at all.

view this post on Zulip Karl Palmskog (Jul 27 2020 at 08:17):

is there a straightforward way to add new "mirrorees" @Théo Zimmermann? Can any one of owners do it?

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 08:19):

Sure. Anton and I can do it. I can add you as an owner of the GitLab organization as well if you confirm to me that @palmskog belongs to you on GitLab.

view this post on Zulip Karl Palmskog (Jul 27 2020 at 08:26):

This is what I get when log in on GitLab: https://gitlab.com/palmskog

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 08:28):

OK, I've just added you.

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 08:30):

Also, if we want to automate the mirroring process, the best would probably to have @coqbot take care of this. Feel free to open an issue on the https://github.com/coq/bot/issues so that we can discuss the requirements.

view this post on Zulip Karl Palmskog (Jul 27 2020 at 08:36):

added the issue, but it gets automatically tagged "bug"? Not sure I understand how that works...

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 08:38):

That's a machine learning bot that does the tagging. You've found a case where it doesn't work.


Last updated: Mar 29 2024 at 13:01 UTC