On Wed, Dec 07, 2022 at 11:29:29AM +0100, Jens Lechtenboerger wrote: > On 2022-12-07, Timothy wrote: [...] > > This seems like an improvement to me, implemented in 56338725e61 :) > > Many thanks, Timothy! Seconded :) -- t