Define the "all" target more reasonably, but retain "html" as the default
target.
diff --git a/Doc/Makefile b/Doc/Makefile
index 8c2c4ed..49608da 100644
--- a/Doc/Makefile
+++ b/Doc/Makefile
@@ -166,7 +166,8 @@
 
 
 # Main target
-all:	html
+default:	html
+all:		html dvi ps pdf isilo
 
 dvi:	$(DVIFILES)
 pdf:	$(PDFFILES)