Michael Tautschnig wrote: [...]
Sorry, there still is an issue here: make user-configured is indeed fine and that stuff is handled nicely in the Makefile, but running make install (in the top-level directory, actually) is troublesome. This causes builds of all the other documents as well, disregarding all the configure stuff. Could you fix that? It might be an option to make the install: target a no-op as well, just as all: is!?
Thanks, Michael
I am not sure I am understanding the issue. Does the problem shows up when you are acting as a "final user" or as a "packager" of the PPL ?
I am asking because yesterday I tried installing the PPL as a final user: I downloaded the latest snapshot, I configured it with all foreign language interfaces _disabled_ (and after having _uninstalled_ ocamldoc, just to be sure) and everything went fine. That is, the manuals that need to be installed by `make install' are already built and distributed in the PPL .tar.gz.
Can you please provide us with the exact sequence of commands leading to the problem?
Thank you in advance, Enea.