On Fri, Aug 25, 2017 at 10:12 PM tim Rowledge <tim@rowledge.org> wrote:

> On 25-08-2017, at 2:49 PM, Fabio Niephaus <lists@fniephaus.com> wrote:
> Did you know that you can edit the file and open a PR directly on GitHub [1]?

Umm, maybe. I have this vague feeling I have actually done that at some point…

Anyway, I did it, saved stuff, opened a pull request etc. Hopefully it actually did what I think it did!

Just merged it and it's live!

tim
--
tim Rowledge; tim@rowledge.org; http://www.rowledge.org/tim
Useful random insult:- IQ = dx / (1 + dx), where x = age.