On Tue, Nov 07, 2017 at 09:58:49PM +0200, Arnold Robbins wrote: > I would just update the .awk file. I think I still have commit access > to the SVN repo, so I'll just do it directly, but I wanted to let > the maintainers know this is coming.
OK fine, I can't see that it would do any harm.
