| changeset 8828 | 5be2d1745c61 |
| parent 8754 | 42ce93ada11e |
| child 8847 | d6c92979fa51 |
--- 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)