On Tue, Oct 16, 2018 at 6:50 AM Junio C Hamano <gits...@pobox.com> wrote: > > Johannes Schindelin <johannes.schinde...@gmx.de> writes: > > > AFAIR Junio does not push to github.com/git/git, it is an automatic > > mirror. > > > > GitLab could easily do the same. > > It used to be in the early days but these days git/git and > gitster/git are updated in a same for loop that pushes to various > destinations. You are correct that GitLab or any other hosting > sites could do the same polling and mirroring. I am just too lazy > to open a new account at yet another hosting site to add that for > loop, but I may choose to when I am absolutely bored and nothing > else to do ;-).
Do you mind if I squat gitlab.com/git/git in the meantime (i.e. create an org etc.) and have it mirror github.com/git/git?, I'll hand the keys over to you if/when you'd like to update your for-loop :) In the meantime sometimes GitLab's UI s better than GitHub's, or the other way around, so it would be useful to have it there as mirror for that reason alone, and then we can always experiment with a .gitlab-ci.yml in-repo.
