equal
deleted
inserted
replaced
7 |
7 |
8 |
8 |
9 FILES = system.tex \ |
9 FILES = system.tex \ |
10 ../iman.sty ../extra.sty |
10 ../iman.sty ../extra.sty |
11 |
11 |
12 system.dvi.gz: $(FILES) |
12 system.dvi.gz: $(FILES) |
|
13 @ln -sf ../isabelle.eps . |
13 -rm system.dvi* |
14 -rm system.dvi* |
14 latex system |
15 latex system |
15 latex system |
16 latex system |
16 ../sedindex system |
17 ../sedindex system |
17 latex system |
18 latex system |
18 gzip -f system.dvi |
19 gzip -f system.dvi |
19 |
20 |
20 dist: $(FILES) |
21 dist: $(FILES) |
|
22 @ln -sf ../isabelle.eps . |
21 -rm system.dvi* |
23 -rm system.dvi* |
22 latex system |
24 latex system |
23 latex system |
25 latex system |
24 ../sedindex system |
26 ../sedindex system |
25 latex system |
27 latex system |