jah Wed Jan 31 12:20:41 2001 EDT
Modified files:
/phpdoc Makefile.in
Log:
Added specific rule to create manual.pdf.
Index: phpdoc/Makefile.in
diff -u phpdoc/Makefile.in:1.51 phpdoc/Makefile.in:1.52
--- phpdoc/Makefile.in:1.51 Tue Jan 23 15:49:44 2001
+++ phpdoc/Makefile.in Wed Jan 31 12:20:40 2001
@@ -26,7 +26,7 @@
# +----------------------------------------------------------------------+
#
-# $Id: Makefile.in,v 1.51 2001/01/23 23:49:44 jimw Exp $
+# $Id: Makefile.in,v 1.52 2001/01/31 20:20:40 jah Exp $
#
VPATH=@srcdir@
@@ -127,6 +127,17 @@
manual.txt.gz: manual.txt
gzip -9 -c $< > $@
+
+manual.pdf: manual.tex
+ # a hack around bugs in jade/jadetex...
+ mv manual.tex manual.tex.tmp
+ sed -e '/HeadingText/,/endHeadPar/ s/_/\\137/g' manual.tex.tmp > manual.tex
+ rm manual.tex.tmp
+
+ jadetex $<
+ jadetex $<
+ jadetex $<
+ dvipdfm -p @PDF_PAPER_TYPE@ manual.dvi
html/index.html: manual.xml $(HTML_DEPS)
@test -d html || mkdir html
