January 8, 2023 at 10:59:54 PM CET Dmitry Gutov <dgutov@yandex.ru> wrote:

On 07/01/2023 12:24, Nicolas Martyanoff wrote:
> 
> FYI This bug seems to have been fixed by
> 899055eef5b212d63e352ada2ac917d13c033a59.
> 

Looks like it indeed.

Brian, would you care to verify?