diff options
Diffstat (limited to 'docs/Makefile')
-rw-r--r-- | docs/Makefile | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/docs/Makefile b/docs/Makefile index 7007e4c982..92ecb20e8f 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -154,6 +154,14 @@ html/man/%.5.html: man/%.pod.5 Makefile $(POD2HTML) --infile=$< --outfile=$@.tmp $(call move-if-changed,$@.tmp,$@) +html/hypercall/stamp: + @$(INSTALL_DIR) $(@D) + ./xen-headers -O $(@D) \ + -T 'arch-x86_64 - Xen public headers' \ + -X arch-ia64 -X arch-x86_32 -X xen-x86_32 \ + ../xen include/public + touch $@ + txt/%.txt: %.txt $(INSTALL_DIR) $(@D) cp $< $@.tmp |