equal
deleted
inserted
replaced
|
1 # |
|
2 # $Id$ |
|
3 # |
|
4 # Common part for Doc Makefiles |
|
5 # |
|
6 |
|
7 ## settings |
|
8 |
|
9 LATEX = latex |
|
10 BIBTEX = bibtex |
|
11 RAIL = rail |
|
12 SEDINDEX = ../sedindex |
|
13 |
|
14 GARBAGE = *.aux *.log *.toc *.idx *.rai *.bbl *.ind *.blg |
|
15 OUTPUT = *.dvi *.pdf *.ps |
|
16 |
|
17 |
|
18 ## actions |
|
19 |
|
20 nothing: |
|
21 |
|
22 clean: |
|
23 @rm -f $(GARBAGE) |
|
24 |
|
25 veryclean: |
|
26 @rm -f $(OUTPUT) $(GARBAGE) |
|
27 |
|
28 isabelle.eps: |
|
29 test -r $* || ln -s ../gfx/$* . |
|
30 |
|
31 isabelle_hol.eps: |
|
32 test -r $* || ln -s ../gfx/$* . |
|
33 |
|
34 isabelle_zf.eps: |
|
35 test -r $* || ln -s ../gfx/$* . |