doc-src/Locales/Makefile
author wenzelm
Wed, 15 Apr 2009 11:14:48 +0200
changeset 30895 bad26d8f0adf
parent 27076 e104481d289d
child 42511 bf89455ccf9d
permissions -rw-r--r--
updated for Isabelle2009;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     1
#
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     2
# $Id$
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     3
#
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     4
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     5
## targets
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     6
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     7
default: dvi
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     8
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     9
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    10
## dependencies
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    11
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    12
include ../Makefile.in
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    13
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    14
NAME = locales
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    15
17135
58f044289dca tuned arrangement of generated stuff;
wenzelm
parents: 16168
diff changeset
    16
FILES = Locales/document/root.tex Locales/document/root.bib \
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26916
diff changeset
    17
  Locales/document/session.tex Locales/document/Examples.tex \
d1d35284542f New version covering interpretation.
ballarin
parents: 26916
diff changeset
    18
  Locales/document/Examples1.tex Locales/document/Examples2.tex \
d1d35284542f New version covering interpretation.
ballarin
parents: 26916
diff changeset
    19
  Locales/document/Examples3.tex \
26916
3331d559feaf use Isabelle sty files from Doc/;
wenzelm
parents: 17135
diff changeset
    20
  ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty 
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    21
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    22
dvi: $(NAME).dvi
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    23
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    24
$(NAME).dvi: $(FILES)
27076
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    25
	cd Locales/document && \
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    26
	$(LATEX) root && \
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    27
	$(BIBTEX) root && \
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    28
	$(LATEX) root && \
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    29
	$(LATEX) root && \
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    30
	$(LATEX) root
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    31
	mv Locales/document/root.dvi $(NAME).dvi
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    32
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    33
pdf: $(NAME).pdf
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    34
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    35
$(NAME).pdf: $(FILES)
27076
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    36
	cd Locales/document && \
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    37
	$(PDFLATEX) root && \
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    38
	$(BIBTEX) root && \
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    39
	$(PDFLATEX) root && \
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    40
	$(PDFLATEX) root && \
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    41
	$(PDFLATEX) root
e104481d289d removed TEXPATH, just chdir to Locales/document;
wenzelm
parents: 27063
diff changeset
    42
	mv Locales/document/root.pdf $(NAME).pdf