aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/Makefile
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1998-12-15 15:50:44 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1998-12-15 15:50:44 +0000
commitb6aef44fd311f42333aae829c2d70d392e3d8848 (patch)
tree53fda0d37b347b99563fe61496c804e83c70956f /doc/Makefile
parentca9ada6119f6834da57f3f1288c6dd46122a7dfe (diff)
Added ps to make all.
Diffstat (limited to 'doc/Makefile')
-rw-r--r--doc/Makefile5
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/Makefile b/doc/Makefile
index 32c5bcc1..80839a17 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -65,11 +65,12 @@ EMACS = xemacs -batch
doc: dvi info
##
-## all : build dvi, html, info
+## all : build dvi, ps, html, info
##
-all: dvi html info
+all: dvi ps html info
dvi: $(DOCNAME).dvi
+ps: $(DOCNAME).ps
pdf: $(DOCNAME).pdf
html: $(DOCNAME).html
info: $(DOCNAME).info