On Sat, 02 May 2020 13:05:00 +0200
Ludovic Courtès <ludo@gnu.org> wrote:

> Hi Björn,
> 
> Björn Höfling <bjoern.hoefling@bjoernhoefling.de> skribis:
> 
> > Fixes <https://debbugs.gnu.org/cgi/bugreport.cgi?bug=40803>.
> > Reported by "operator.name" <operator.name@protonmail.com>.
> >

> LGTM!
> 
> Thanks,
> Ludo’.

Thanks,

pushed as 7c65fc378cf68b598965fd977f5844050435ac97.

Björn