docs should not have unused files
reference-manual-minimal and user-guide-old should not exist any more. Are there are other remaining things left behind from the migration to sphinx?
Remove unused files in docs/manual
#2 Updated by Paul Bauer 11 months ago
The reference-manual-minimal and user-guide-old files are kind of needed, because they are used when the image conversion (and thus build) fail for the reference manual and the webpage build falls back to build a minimal version without it.
The conversion-friendly folder should go, though (I even forgot it was still there).
#4 Updated by Mark Abraham 11 months ago
OK. "old" doesn't really help people in three years know what it is for. Naming things for what they are now helps, because that should still be true later on :-)
How about naming things
and a comment in the first two .rst files that explains why they are crippled. If they're off in another directory, and not built in Jenkins, the build is sure to rot. In the same directory, they might get noticed and remembered.