# HG changeset patch
# User wenzelm
# Date 925920458 -7200
# Node ID 62204772812f7b801b87274a5302e0cca7f33d48
# Parent  c120262044b6b7e2ff2a880f76b2a2f4b23f8b1c
Common part for Doc Makefiles;

diff -r c120262044b6 -r 62204772812f doc-src/Makefile.in
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Makefile.in	Wed May 05 18:07:38 1999 +0200
@@ -0,0 +1,35 @@
+#
+# $Id$
+#
+# Common part for Doc Makefiles
+#
+
+## settings
+
+LATEX = latex
+BIBTEX = bibtex
+RAIL = rail
+SEDINDEX = ../sedindex
+
+GARBAGE = *.aux *.log *.toc *.idx *.rai *.bbl *.ind *.blg
+OUTPUT = *.dvi *.pdf *.ps
+
+
+## actions
+
+nothing:
+
+clean:
+	@rm -f $(GARBAGE)
+
+veryclean:
+	@rm -f $(OUTPUT) $(GARBAGE)
+
+isabelle.eps:
+	test -r $* || ln -s ../gfx/$* .
+
+isabelle_hol.eps:
+	test -r $* || ln -s ../gfx/$* .
+
+isabelle_zf.eps:
+	test -r $* || ln -s ../gfx/$* .