diff options
author | Graham Christensen <graham@grahamc.com> | 2018-10-02 15:59:00 -0400 |
---|---|---|
committer | Graham Christensen <graham@grahamc.com> | 2018-10-02 15:59:00 -0400 |
commit | 444e04b98571ad65269c8a988c4a9f772ca616a2 (patch) | |
tree | 74d84758495ab25664bf4d40e0b15d1b31bee348 /doc/Makefile | |
parent | c3125498fd7d0398f50e2b53a9e274b7c1e2db67 (diff) |
nixpkgs docs: Rebuild manual-full if nested XML docs change
Diffstat (limited to 'doc/Makefile')
-rw-r--r-- | doc/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
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: |