Gerd Aschemann In fact, this change is rather simple and straightforward, so I suggest you provide a Pull Request with the fix I mentioned above. This is, typically, the most efficient way to get a fix.