doc-src/System/Makefile
changeset 5170 33fbffd06c12
parent 3172 629d63c74ddc
child 5374 6ef3742b6153
     1.1 --- a/doc-src/System/Makefile	Tue Jul 21 16:38:25 1998 +0200
     1.2 +++ b/doc-src/System/Makefile	Tue Jul 21 16:41:12 1998 +0200
     1.3 @@ -9,7 +9,8 @@
     1.4  FILES =  system.tex \
     1.5  	 ../iman.sty ../extra.sty
     1.6  
     1.7 -system.dvi.gz:   $(FILES) 
     1.8 +system.dvi.gz:   $(FILES)
     1.9 +	@ln -sf ../isabelle.eps .
    1.10  	-rm system.dvi*
    1.11  	latex system
    1.12  	latex system
    1.13 @@ -17,7 +18,8 @@
    1.14  	latex system
    1.15  	gzip -f system.dvi
    1.16  
    1.17 -dist:   $(FILES) 
    1.18 +dist:   $(FILES)
    1.19 +	@ln -sf ../isabelle.eps .
    1.20  	-rm system.dvi*
    1.21  	latex system
    1.22  	latex system