diff --git a/Doc/Makefile b/Doc/Makefile
index b3e281f..a086769 100644
--- a/Doc/Makefile
+++ b/Doc/Makefile
@@ -175,6 +175,9 @@
 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)