Re: Git repository mirror is out of date

[Karl Berry]

    It is confusing to have it there but be out-of-date, so in that
    case would you mind disabling it?

I did that.