Bruno Haible Thu, 21 May 2020 07:33:21 -0700
> The attached patch fixes it. (Please feel free to amend.) Thanks, I've pushed it in your name.
Bruno