Diff of /manual/Makefile

Parent Directory | Revision Log | Revision Graph | Patch

--- manual/Makefile	2002/04/24 18:02:50	1.14
+++ manual/Makefile	2002/04/24 20:48:16	1.15
@@ -15,6 +15,7 @@
 	make tex
 	make ps
 	make pdf
+	make ps.gz
 	make html
 
 tex:
@@ -25,6 +26,9 @@
 
 ps: manual.ps
 
+ps.gz: manual.ps
+	gzip -9 -c manual.ps > manual.ps.gz
+
 pdf: manual.pdf
 
 manual.ps: manual.dvi