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