doc-src/Locales/Makefile
author haftmann
Tue Sep 22 15:39:46 2009 +0200 (2009-09-22)
changeset 32697 72e8608dce54
parent 27076 e104481d289d
child 42511 bf89455ccf9d
permissions -rw-r--r--
merged
     1 #
     2 # $Id$
     3 #
     4 
     5 ## targets
     6 
     7 default: dvi
     8 
     9 
    10 ## dependencies
    11 
    12 include ../Makefile.in
    13 
    14 NAME = locales
    15 
    16 FILES = Locales/document/root.tex Locales/document/root.bib \
    17   Locales/document/session.tex Locales/document/Examples.tex \
    18   Locales/document/Examples1.tex Locales/document/Examples2.tex \
    19   Locales/document/Examples3.tex \
    20   ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty 
    21 
    22 dvi: $(NAME).dvi
    23 
    24 $(NAME).dvi: $(FILES)
    25 	cd Locales/document && \
    26 	$(LATEX) root && \
    27 	$(BIBTEX) root && \
    28 	$(LATEX) root && \
    29 	$(LATEX) root && \
    30 	$(LATEX) root
    31 	mv Locales/document/root.dvi $(NAME).dvi
    32 
    33 pdf: $(NAME).pdf
    34 
    35 $(NAME).pdf: $(FILES)
    36 	cd Locales/document && \
    37 	$(PDFLATEX) root && \
    38 	$(BIBTEX) root && \
    39 	$(PDFLATEX) root && \
    40 	$(PDFLATEX) root && \
    41 	$(PDFLATEX) root
    42 	mv Locales/document/root.pdf $(NAME).pdf