Karl Palmskog (Jul 27 2020 at 08:15): 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.
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?
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.
Karl Palmskog (Jul 27 2020 at 08:26):This is what I get when log in on GitLab: https://gitlab.com/palmskog
Théo Zimmermann (Jul 27 2020 at 08:28):OK, I've just added you.
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.
Karl Palmskog (Jul 27 2020 at 08:36):added the issue, but it gets automatically tagged "bug"? Not sure I understand how that works...
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: Jun 06 2023 at 22:01 UTC