diff --git a/Doc/Makefile b/Doc/Makefile index b3e281f38049..a086769ea247 100644 --- a/Doc/Makefile +++ b/Doc/Makefile @@ -175,6 +175,9 @@ html: htmlapi: (cd $(HTMLDIR); $(MAKE) PAPER=$(PAPER) -f ../html/Makefile api) +htmldoc: + (cd $(HTMLDIR); $(MAKE) PAPER=$(PAPER) -f ../html/Makefile doc) + htmlext: (cd $(HTMLDIR); $(MAKE) PAPER=$(PAPER) -f ../html/Makefile ext)