improved Makefile

diff --git a/helm/ocaml/cic_notation/doc/Makefile b/helm/ocaml/cic_notation/doc/Makefile
index 4db53fdf05e25bf53ae9a9be00309de06e28bfb3..b7d8fb45cfdf520bd50cd5c895702f4b2f16747e 100644 (file)
--- a/helm/ocaml/cic_notation/doc/Makefile
+++ b/helm/ocaml/cic_notation/doc/Makefile
@@ -5,7 +5,7 @@
 # Author: Stefano Zacchiroli <zack@bononia.it>
 #
 # Created:       Sun, 29 Jun 2003 12:00:55 +0200 zack
-# Last-Modified: Tue, 05 Apr 2005 10:25:38 +0200 zack
+# Last-Modified: Mon, 10 Oct 2005 15:37:12 +0200 zack
 #
 
 ########################################################################
@@ -44,9 +44,10 @@ GZIP = gzip
 HEVEA = hevea
 ISPELL = ispell
 LATEX = latex
+PDFLATEX = pdflatex
+PRINT = lpr
 XDVI = xdvi
 XPDF = xpdf
-PDFLATEX = pdflatex
 
 ALL_FORMATS = $(BUILD_FORMATS)
 WORLD_FORMATS = $(AVAILABLE_FORMATS)
@@ -79,6 +80,9 @@ showps.gz: showpsgz
 showhtml: $(HTMLS)
        $(BROWSER) $<
 
+print: $(PSS)
+       $(PRINT) $^
+
 clean:
        rm -f \
                $(TEXS:.tex=.dvi) $(TEXS:.tex=.ps) $(TEXS:.tex=.ps.gz) \