On 2020-08-30 14:30, Tomasz Buchert wrote: > It seems you have already done this :). Yes, right now. Sorry for pushing this. > Good, makes sense to me. I assumed, that this change were not controversial ;-)