Added "html" and "info" goals to the top-level Makefile.

They are for people who don't want to build both types of documents at the same time.

diff --git a/Makefile b/Makefile
index 808689c82942be7696a935122e3fc21189901e76..206f853fc98ea1921022895c209f6bbd2c68755c 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-.PHONY: all mostlyclean clean install zip avail unavail bin lib doc samples
+.PHONY: all mostlyclean clean install zip avail unavail bin lib doc html info samples
 
 .SUFFIXES:
 
@@ -14,7 +14,7 @@ avail unavail bin:
 lib:
        @$(MAKE) -C libsrc  --no-print-directory $@
 
-doc:
+doc html info:
        @$(MAKE) -C doc     --no-print-directory $@
 
 samples: