On Fri, Jul 27, 2018 at 11:38:08AM +0200, Bruno Haible wrote: > Paul Eggert wrote: > > I looked at it just now; seems OK, and I installed it. Thanks. > > I added a corresponding ChangeLog entry.
Thanks to you both; I'm sorted now (and rather belatedly a convert to using bootstrap rather than keeping generated files in git). -- Colin Watson [cjwat...@debian.org]