equal
deleted
inserted
replaced
3 # |
3 # |
4 |
4 |
5 ## targets |
5 ## targets |
6 |
6 |
7 default: dvi |
7 default: dvi |
8 dist: dvi |
|
9 |
8 |
10 |
9 |
11 ## dependencies |
10 ## dependencies |
12 |
11 |
13 include ../Makefile.in |
12 include ../Makefile.in |
24 $(BIBTEX) $(NAME) |
23 $(BIBTEX) $(NAME) |
25 $(LATEX) $(NAME) |
24 $(LATEX) $(NAME) |
26 $(LATEX) $(NAME) |
25 $(LATEX) $(NAME) |
27 $(SEDINDEX) $(NAME) |
26 $(SEDINDEX) $(NAME) |
28 $(LATEX) $(NAME) |
27 $(LATEX) $(NAME) |
|
28 |
|
29 pdf: $(NAME).pdf |
|
30 |
|
31 $(NAME).pdf: $(FILES) isabelle_hol.pdf |
|
32 touch $(NAME).ind |
|
33 $(PDFLATEX) $(NAME) |
|
34 $(BIBTEX) $(NAME) |
|
35 $(PDFLATEX) $(NAME) |
|
36 $(PDFLATEX) $(NAME) |
|
37 $(SEDINDEX) $(NAME) |
|
38 $(FIXBOOKMARKS) $(NAME).out |
|
39 $(PDFLATEX) $(NAME) |