diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/TutorialI/Makefile
--- a/doc-src/TutorialI/Makefile	Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/TutorialI/Makefile	Mon May 08 11:13:28 2000 +0200
@@ -19,7 +19,6 @@
 dvi: $(NAME).dvi
 
 $(NAME).dvi: $(FILES) isabelle_hol.eps
-	touch $(NAME).ind
 	$(LATEX) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(LATEX) $(NAME)
@@ -30,7 +29,6 @@
 pdf: $(NAME).pdf
 
 $(NAME).pdf: $(FILES) isabelle_hol.pdf
-	touch $(NAME).ind
 	$(PDFLATEX) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(PDFLATEX) $(NAME)