On Sat, 3 Nov 2018, Vincent Privat wrote:
By the way the script doesn't work anymore, I was unable to update the strings for last release.
Someone replaced a bold small dot with a large normal dot in the wiki :-) Fixed and Updated. Whoa takes it long nowadays...(We could optimize and parallelize the access, but I doubt wiki admins will be happy about that :-)
Ciao -- http://www.dstoecker.eu/ (PGP key available)
