diff --git a/doc/Makefile b/doc/Makefile index ba77be6678c4..173e1c0b19ee 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -69,7 +69,7 @@ highlightjs: cp -r "$$HIGHLIGHTJS/loader.js" highlightjs/ -manual-full.xml: ${MD_TARGETS} .version *.xml +manual-full.xml: ${MD_TARGETS} .version *.xml **/*.xml xmllint --nonet --xinclude --noxincludenode manual.xml --output manual-full.xml .version: