--- a/doc-src/Intro/Makefile Fri May 07 17:49:32 1999 +0200
+++ b/doc-src/Intro/Makefile Fri May 07 17:50:43 1999 +0200
@@ -30,7 +30,7 @@
pdf: $(NAME).pdf
-$(NAME).pdf: $(FILES) isabelle.png
+$(NAME).pdf: $(FILES) isabelle.pdf
touch $(NAME).ind
$(PDFLATEX) $(NAME)
$(BIBTEX) $(NAME)