diff -r 29f09a778037 -r 5cd3396802f5 doc-src/System/Makefile --- a/doc-src/System/Makefile Thu Sep 24 15:23:47 1998 +0200 +++ b/doc-src/System/Makefile Thu Sep 24 15:36:16 1998 +0200 @@ -10,7 +10,7 @@ ../iman.sty ../extra.sty system.dvi.gz: $(FILES) - @ln -sf ../gfx/isabelle.eps . + test -r isabelle.eps || ln -s ../gfx/isabelle.eps . -rm system.dvi* latex system latex system @@ -19,7 +19,7 @@ gzip -f system.dvi dist: $(FILES) - @ln -sf ../gfx/isabelle.eps . + test -r isabelle.eps || ln -s ../gfx/isabelle.eps . -rm system.dvi* latex system latex system