I'm having a look at how the extracted documentation is built, because I think there's supposed to be some infrastructure for extracting and installing documentation from third-party modules built with the help of pike -x module, and I doubt that it will work the current packaging.

IIUC, "make documentation" first uses extract_autodoc to create one XML file with documentation per source file (placed under the doc_build subdirectory of the build directory), then join_autodoc to create autodoc.xml from these, then assemble_autodoc to create modref.xml, traditional.xml, and onepage.xml with the help of templates. Last, make is run in the refdoc directory. There, tree-split-autodoc.pike and make_html.pike (in refdoc/presentation) produce the HTML and put it in refdoc/modref and refdoc/traditional_manual, respectively.

Now, in install.pike there is code to install autodoc.xml (as core_autodoc.xml) as well as images, templates, the aforementioned Pike scripts, and modref/Makefile into $(doc_prefix)/src. It doesn't install the generated HTML though. I wonder if refdoc/Makefile was meant to do that, because it prefixes *most* destination directories with $(DESTDIR), but DESTDIR is never set.

Or wait, common_module_makefile.in actually sets DESTDIR to $(SYSTEM_DOC_PATH), i.e. doc_prefix. So if I guess correctly, pike -x module --make modref in a module source directory is meant to extract the documentation from the module, join it with the core module documentation and place the resulting HTML in the correct place. I'm not sure if that module's documentation will be kept if the same is done with another module, however.

Have I understood correctly? What is the status of this system, especially considering that dynamic_module_makefile is deprecated?