summaryrefslogtreecommitdiff
path: root/doc/Makefile
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-27 14:38:53 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-27 14:38:53 -0500
commit85a682b4a65a76e2f5a120b28faf7093f4a766a9 (patch)
tree3f180b88f47fe8cfb1f6dda748baf30d41363b56 /doc/Makefile
parent9004ba508ee89c4fe4b758ffe0f87518b48670ae (diff)
Start of manual
Diffstat (limited to 'doc/Makefile')
-rw-r--r--doc/Makefile23
1 files changed, 23 insertions, 0 deletions
diff --git a/doc/Makefile b/doc/Makefile
new file mode 100644
index 00000000..777c5bf7
--- /dev/null
+++ b/doc/Makefile
@@ -0,0 +1,23 @@
+PAPERS=manual
+
+FIGURES=
+
+all: $(PAPERS:%=%.dvi) $(PAPERS:%=%.ps) $(PAPERS:%=%.pdf)
+
+%.dvi: %.tex $(FIGURES:%=%.eps)
+ latex $<
+ latex $<
+
+%.ps: %.dvi
+ dvips $< -o $@
+
+%.pdf: %.dvi $(FIGURES:%=%.pdf)
+ pdflatex $(<:%.dvi=%)
+
+%.pdf: %.eps
+ epstopdf $<
+
+clean:
+ rm -f *.aux *.bbl *.blg *.dvi *.log *.pdf *.ps
+
+.PHONY: all clean