Define the "all" target more reasonably, but retain "html" as the default

target.

diff --git a/Doc/Makefile b/Doc/Makefile
index 8c2c4eded0df30fb0d20f601039c12de2204b655..49608dab93ec084cb7e722f265786d3a2ac92e90 100644 (file)
--- 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)