On Mon, Oct 08, 2018 at 08:40:49AM +0200, Laurenz Albe wrote:> I'm fine with it.
Thanks, I have pushed this version and back-patched to v11.--Michael