equal
deleted
inserted
replaced
6 |
6 |
7 default: dvi |
7 default: dvi |
8 |
8 |
9 ## paths |
9 ## paths |
10 |
10 |
11 TEXPATH = Locales/generated/: |
11 TEXPATH = Locales/document/: |
12 |
12 |
13 ## dependencies |
13 ## dependencies |
14 |
14 |
15 include ../Makefile.in |
15 include ../Makefile.in |
16 |
16 |
17 NAME = locales |
17 NAME = locales |
18 |
18 |
19 FILES = Locales/generated/root.tex Locales/generated/root.bib \ |
19 FILES = Locales/document/root.tex Locales/document/root.bib \ |
20 Locales/generated/session.tex Locales/generated/Locales.tex \ |
20 Locales/document/session.tex Locales/document/Locales.tex \ |
21 Locales/generated/isabelle.sty Locales/generated/isabellesym.sty \ |
21 Locales/document/isabelle.sty Locales/document/isabellesym.sty \ |
22 Locales/generated/pdfsetup.sty |
22 Locales/document/pdfsetup.sty |
23 |
23 |
24 dvi: $(NAME).dvi |
24 dvi: $(NAME).dvi |
25 |
25 |
26 $(NAME).dvi: $(FILES) |
26 $(NAME).dvi: $(FILES) |
27 env TEXINPUTS=$(TEXPATH) $(LATEX) root |
27 env TEXINPUTS=$(TEXPATH) $(LATEX) root |