Oops! Must have deleted a word by accident before the last check-in of this

file; "make" (the 'all' target) became a no-op!

Now works as previously described.

diff --git a/Doc/Makefile b/Doc/Makefile
index f080215963d081ab6cfd01c175bc84655228ae99..b8d0535aae35cf566cce877bdea0c08a9c5c9e81 100644 (file)
--- a/Doc/Makefile
+++ b/Doc/Makefile
@@ -89,7 +89,7 @@ MKHTML=               TEXINPUTS=$(TEXINPUTS) $(srcdir)/tools/mkhtml.sh
 MKPDF=         TEXINPUTS=$(TEXINPUTS) $(srcdir)/tools/mkdvi.sh --pdf
 
 # Main target
-all:
+all:   all-ps
 
 all-dvi:
        (cd paper-$(PAPER); $(MAKE) all-dvi)