equal
deleted
inserted
replaced
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 @ln -sf ../gfx/isabelle.eps . |
14 -rm system.dvi* |
14 -rm system.dvi* |
15 latex system |
15 latex system |
16 latex system |
16 latex system |
17 ../sedindex system |
17 ../sedindex system |
18 latex system |
18 latex system |
19 gzip -f system.dvi |
19 gzip -f system.dvi |
20 |
20 |
21 dist: $(FILES) |
21 dist: $(FILES) |
22 @ln -sf ../isabelle.eps . |
22 @ln -sf ../gfx/isabelle.eps . |
23 -rm system.dvi* |
23 -rm system.dvi* |
24 latex system |
24 latex system |
25 latex system |
25 latex system |
26 ../sedindex system |
26 ../sedindex system |
27 latex system |
27 latex system |