doc-src/Locales/Makefile

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Locales/Makefile	Fri Apr 16 11:35:44 2004 +0200
@@ -0,0 +1,40 @@
+#
+# $Id$
+#
+
+## targets
+
+default: dvi
+
+## paths
+
+TEXPATH = Locales/generated/:
+
+## dependencies
+
+include ../Makefile.in
+
+NAME = locales
+
+FILES = locales.tex Locales/generated/root.bib \
+  Locales/generated/session.tex Locales/generated/Locales.tex \
+  Locales/generated/isabelle.sty Locales/generated/isabellesym.sty \
+  Locales/generated/pdfsetup.sty 
+
+dvi: $(NAME).dvi
+
+$(NAME).dvi: $(FILES)
+	env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME)
+	env BIBINPUTS=$(TEXPATH) $(BIBTEX) $(NAME)
+	env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME)
+	env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME)
+	env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME)
+
+pdf: $(NAME).pdf
+
+$(NAME).pdf: $(FILES)
+	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME)
+	env BIBINPUTS=$(TEXPATH) $(BIBTEX) $(NAME)
+	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME)
+	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME)
+	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME)