Paul Eggert Fri, 11 Aug 2017 12:57:14 -0700
On 08/11/2017 11:46 AM, Bruno Haible wrote:
This should fix it:
Ah, thanks, please ignore my previous message on this topic.