[Dune-devel] Mirroring to Github

[Dominic Kempf]

Dear Dune developers,

I have taken the liberty to clean up the mirroring of our repositories to
Github and recover all the necessary access etc. Here are some thoughts
about the process that I would like to share:

* The mirroring is now done using a Gitlab built-in functionality. You find
it in Settings/Repository/Mirroring Repositories. Everybody with enough
privileges can do that. Before, this was a cronjob on a private server by
Ansgar. I am very grateful Ansgar has provided this service, but I think a
configuration that is visible to all current and future core developers is
better.
* I toggled the setting "Only Mirror Protected Branches" (here: master +
releases/*). This might be controversial, but before my cleanup our
repositories on Github all had between 100-500 branches because the
mirroring added all new branches, but never deleted some (include
cherrypick-* branches).
* I have adjusted the Github Project description to explicitly point to our
Gitlab instance.
* I am now a member of the dune-project organization (
https://github.com/dune-project) and can make you one too, if you wish to
mirror a repository into that group. Just send me a mail.

I hope everybody is fine with these changes,

Best,
Dominic

PS: I have also recovered credentials for the duneci organization of
DockerHub and the dune-project organization on Gitlab.com, but I have not
done anything with these yet.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.dune-project.org/pipermail/dune-devel/attachments/20210129/de907b60/attachment.htm>