diff --git a/Doc/Makefile b/Doc/Makefile
index 8c2c4eded0d..49608dab93e 100644
--- a/Doc/Makefile
+++ b/Doc/Makefile
@@ -166,7 +166,8 @@ include Makefile.deps
 
 
 # Main target
-all:	html
+default:	html
+all:		html dvi ps pdf isilo
 
 dvi:	$(DVIFILES)
 pdf:	$(PDFFILES)