-
Gunter Königsmann authored
Part of what made the documentation build system hard to maintain was that each manual translation used slightly different methods for doing the same thing: Compiling a manual. Additionally there are many historical left-overs of which one (the Microsoft HTML Help workshop version) definitely no was is in use. After this change the manuals should all build in more-or-less similar ways and using a smaller number of unnecessary steps.