doc-src/System/Makefile
changeset 5548 5cd3396802f5
parent 5374 6ef3742b6153
child 6600 5a94bd71cc41
equal deleted inserted replaced
5547:29f09a778037 5548:5cd3396802f5
     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 ../gfx/isabelle.eps .
    13 	test -r isabelle.eps || ln -s ../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 ../gfx/isabelle.eps .
    22 	test -r isabelle.eps || ln -s ../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