Markus Schade Fri, 26 Oct 2018 02:45:49 -0700
Hi Christoph, Yes, this is somewhat annoying. I don't see how we could change this behavior besides patching this in source. Which I don't think is really justified.
Best regards, Markus
