Hi,

On Wed, 18 Nov 2020 22:26:38 +0100
Marius Bakke <marius@gnu.org> wrote:

> I suspect this was fixed by 37b98e8cca3244067071bc6e382b06861457a459,
> can you confirm?

Yes, it is indeed fixed for me.