diff -r eb87300379fe -r 2d56911d7329 doc-src/Intro/Makefile
--- 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)