On 6/17/20, Valentin Villenave <valen...@villenave.net> wrote: > Thanks for giving me hope, even for a minute :-)
I spoke too soon; running doc-clean and _then_ “make doc” indeed fixes the problem. (And Jonas has just merged it onto master so that problem is fixed.) Thanks! Cheers, -- V.
