Hi Paul, On 11 Mar 2013, at 12:31, Paul Eggert <[email protected]> wrote: > On 03/10/2013 10:18 PM, Gary V. Vaughan wrote: >> Any objections if I push the fix? > > No, thanks, that fix looks good to me.
Pushed. Thank you. Cheers, -- Gary V. Vaughan (gary AT gnu DOT org)
