On 28/03/2023 09:54, Paul Eggert wrote:
> Thanks for reporting that. I installed the attached to fix it.

Looks good thanks.
Also worth the attached test and NEWS,
which I've pushed.

cheers,
Pádraig