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!
tim -- tim Rowledge; tim@rowledge.org; http://www.rowledge.org/tim Useful random insult:- IQ = dx / (1 + dx), where x = age.