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