On Sun, Oct 20, 2013 at 4:08 PM, Paul Eggert <[email protected]> wrote: > Closing, as I've already patched this. I guess I shouldn't send > email of installed fixes to bug-grep; sorry, I always forget > which projects do that and which don't.
No problem at all. Your choice.
