doc-src/Locales/Makefile
author ballarin
Tue Jun 03 12:34:22 2008 +0200 (2008-06-03)
changeset 27063 d1d35284542f
parent 26916 3331d559feaf
child 27076 e104481d289d
permissions -rw-r--r--
New version covering interpretation.
     1 #
     2 # $Id$
     3 #
     4 
     5 ## targets
     6 
     7 default: dvi
     8 
     9 ## paths
    10 
    11 TEXPATH = Locales/document/:
    12 
    13 ## dependencies
    14 
    15 include ../Makefile.in
    16 
    17 NAME = locales
    18 
    19 FILES = Locales/document/root.tex Locales/document/root.bib \
    20   Locales/document/session.tex Locales/document/Examples.tex \
    21   Locales/document/Examples1.tex Locales/document/Examples2.tex \
    22   Locales/document/Examples3.tex \
    23   ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty 
    24 
    25 dvi: $(NAME).dvi
    26 
    27 $(NAME).dvi: $(FILES)
    28 	env TEXINPUTS=$(TEXPATH) $(LATEX) root
    29 	env BIBINPUTS=$(TEXPATH) $(BIBTEX) root
    30 	env TEXINPUTS=$(TEXPATH) $(LATEX) root
    31 	env TEXINPUTS=$(TEXPATH) $(LATEX) root
    32 	env TEXINPUTS=$(TEXPATH) $(LATEX) root
    33 	mv root.dvi $(NAME).dvi
    34 
    35 pdf: $(NAME).pdf
    36 
    37 $(NAME).pdf: $(FILES)
    38 	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) root
    39 	env BIBINPUTS=$(TEXPATH) $(BIBTEX) root
    40 	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) root
    41 	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) root
    42 	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) root
    43 	mv root.pdf $(NAME).pdf