Worked for me™
I'll look into it right away.
On 11/27/18 7:13 PM, Neels Hofmeyr wrote:
Hi Oliver,
so I merged the stuff to add the manuals to the individual git repositories, since you said that it works. But when I do --enable-manuals I don't see any PDF files generated. Also a manual 'make pdf' says "nothing to be done".
(I probably should have tried it before merging after all)
So what am I doing wrong? Alternatively, can you fix it please?
~N