On December 27, 2012 at 12:42 PM "Pádraig Brady" <p...@draigbrady.com> wrote: > On 12/26/2012 07:43 AM, Akim Demaille wrote: > I've adjusted things a bit in the attached patch,
Looks good. As it was reported as a bug, shouldn't we mention it in the commit message: - Reported by Akim Demaille. + Reported by Akim Demaille in http://bugs.gnu.org/13280. and (maybe even) in NEWS? For NEWS, the change may be too marginal, but at least a reference in Git would be great IMO. Have a nice day, Berny
