equal
deleted
inserted
replaced
9 LATEX = latex |
9 LATEX = latex |
10 BIBTEX = bibtex |
10 BIBTEX = bibtex |
11 RAIL = rail |
11 RAIL = rail |
12 SEDINDEX = ../sedindex |
12 SEDINDEX = ../sedindex |
13 |
13 |
14 GARBAGE = *.aux *.log *.toc *.idx *.rai *.rao *.bbl *.ind *.blg |
14 GARBAGE = *.aux *.log *.toc *.idx *.rai *.rao *.bbl *.ind *.blg *.out |
15 OUTPUT = *.dvi *.pdf *.ps |
15 OUTPUT = *.dvi *.pdf *.ps |
16 |
16 |
17 |
17 |
18 ## actions |
18 ## actions |
19 |
19 |
20 nothing: |
20 nothing: |
21 |
21 |
22 clean: |
22 clean: |
23 @rm -f $(GARBAGE) |
23 @rm -f $(GARBAGE) |
24 |
24 |
25 veryclean: |
25 mrproper: |
26 @rm -f $(OUTPUT) $(GARBAGE) |
26 @rm -f $(OUTPUT) $(GARBAGE) |
27 |
27 |
28 isabelle.eps: |
28 isabelle.eps: |
29 test -r $* || ln -s ../gfx/$* . |
29 test -r $* || ln -s ../gfx/$* . |
30 |
30 |