Use docbook to build manual.pdf; clean *.xml files