On 20 August 2015 at 23:32, Jason Merrill wrote: > On 08/20/2015 04:33 PM, Joseph Myers wrote: >> * Make sure whatever process updates the github mirror is kept going after >> the conversion (actually it looks like it broke two weeks ago...). > > > I have no idea how this mirror is updated. Its github page is remarkably > uninformative.
AFAIK it's nothing official, just set up by someone out in the interwebs, and it is always broken. It has all the commits, but doesn't move the trunk and master refs correctly. I don't think it should have any bearing on transitioning the official repo to git.
