GitLab mirror considered harmful

[Michael Gratton <mike vee net>]

Hi all,

While the GitHub mirror may have been useful back before GitLab, it 
actually discourages contributions because PRs aren't accepted there. I've 
not seen from any positive outcomes from it that I can remember, only 
negative ones. As such I think it should be deleted.

Because of this I just filed: 
https://gitlab.gnome.org/Infrastructure/Infrastructure/issues/86​ – any 
thoughts?

//Mike