On 6/20/21 3:15 PM, Bruno Haible wrote:
> Can someone please deal with this? Simon? Akim? Berny? Not always me :-)

Something like the attached patch perhaps? (I haven't tested or 
installed it.)