<div dir="ltr"><div>Dear Dune developers,</div><div><br></div><div>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:</div><div><br></div><div>* 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.</div><div>* 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).<br></div><div>* I have adjusted the Github Project description to explicitly point to our Gitlab instance.</div><div>* I am now a member of the dune-project organization (<a href="https://github.com/dune-project" target="_blank">https://github.com/dune-project</a>) and can make you one too, if you wish to mirror a repository into that group. Just send me a mail.</div><div><br></div><div>I hope everybody is fine with these changes,<br></div><div><br></div><div>Best,</div><div>Dominic</div><div><br></div><div>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.<div class="gmail-adL"><br><br></div></div></div>