Oct. 29, 2017
7:22 a.m.
Thanks for the heads-up. I installed the attached patches into the development version. The first one is your patch, but with a slightly altered commit message. The second adds a NEWS item about the change, and alters the spelling of your name to be what I hope is the proper one since the source code allows UTF-8 in comments. (If you prefer the Anglicized spelling, please let me know.)