Hi Paul, On 11 Mar 2013, at 12:31, Paul Eggert <egg...@cs.ucla.edu> 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)
