Use a general mechanism of storing all job variables for each build job
separately, so that we have all documentation files in the
FILES_documentation variable. This makes the dedicated HTML_FILES
variable obsolete.
The merged variables are still kept, though, so that we have all
machines in the MACHINE variable to loop over.