doc-src/System/Makefile
changeset 8828 5be2d1745c61
parent 7207 ad69aa13ddf6
child 9695 ec7d7f877712
     1.1 --- a/doc-src/System/Makefile	Mon May 08 11:13:11 2000 +0200
     1.2 +++ b/doc-src/System/Makefile	Mon May 08 11:13:28 2000 +0200
     1.3 @@ -18,7 +18,6 @@
     1.4  dvi: $(NAME).dvi
     1.5  
     1.6  $(NAME).dvi: $(FILES) isabelle.eps
     1.7 -	touch $(NAME).ind
     1.8  	$(LATEX) $(NAME)
     1.9  	$(BIBTEX) $(NAME)
    1.10  	$(LATEX) $(NAME)
    1.11 @@ -29,7 +28,6 @@
    1.12  pdf: $(NAME).pdf
    1.13  
    1.14  $(NAME).pdf: $(FILES) isabelle.pdf
    1.15 -	touch $(NAME).ind
    1.16  	$(PDFLATEX) $(NAME)
    1.17  	$(BIBTEX) $(NAME)
    1.18  	$(PDFLATEX) $(NAME)