Re: FYI: gnulib git mirror is up to date

[Karl Berry]

    BTW, Karl, I notice a lot of "." log entries in your name.  I presume most
    are done automatically.

For MODULES.html, yes.  Everything else I commit by hand.

  name-of-script: regenerate MODULES.html

There is no separate script, and anyway, given below, never mind.

    generate it into the savannah web repo instead:
      http://web.cvs.savannah.gnu.org/viewcvs/gnulib/?root=gnulib

That sounds fine to me.  Do you want me to do it now, or do you want to
do it as part of the git stuff, or what?