Added targets dvi, pdf, and ps, to make all of the documents in those formats.

diff --git a/Doc/Makefile b/Doc/Makefile
index cb6008e159063dda639d59144b35f04ab6f31977..1ab0c13505dbdb520782d87a36399121998f1d61 100644 (file)
--- a/Doc/Makefile
+++ b/Doc/Makefile
@@ -90,17 +90,17 @@ MKPDF=              TEXINPUTS=$(TEXINPUTS) $(srcdir)/tools/mkdvi.sh --pdf
 # Main target
 all:   all-ps
 
-all-dvi:
+all-dvi dvi:
        (cd paper-$(PAPER); \
                $(MAKE) srcdir=.. VPATH=.. TEXINPUTS=$(TEXINPUTS) \
                -f ../Makefile do-dvi)
 
-all-pdf:
+all-pdf pdf:
        (cd paper-$(PAPER); \
                $(MAKE) srcdir=.. VPATH=.. TEXINPUTS=$(TEXINPUTS) \
                -f ../Makefile do-pdf)
 
-all-ps:
+all-ps ps:
        (cd paper-$(PAPER); \
                $(MAKE) srcdir=.. VPATH=.. TEXINPUTS=$(TEXINPUTS) \
                -f ../Makefile do-ps)