Re: Git repository mirror is out of date

[Karl Berry]

    I checked out the Git mirror of the Texinfo repository today, to
    figure out whether some bugs had been fixed, and I noticed that
    it contains no commits newer than 2009-04-21.  Since the CVS
    repository contains much newer files, I guess the Git repository
    is out-of-date.  If it is synced manually, then it's time!

It's not supposed to be manual.  But I didn't set up the git mirror and
don't use it.

Jim, can you deal with this?  If I'm recalling correctly that you were
the one who wanted and created it.  Or, I'm happy to drop it :).

Thanks,
K