On Tuesday, 15 May 2018 11.03.01 WEST Jean-Marc Lasgouttes wrote: > This has been fixed by Enrico at 6253cc4c51e4e3, right? > > JMarc
After running again autogen.sh the problem went away. So I suspect that the answer is yes to your question. :-) -- José Abílio