| changeset 6611 | 08dfd050b373 |
| parent 6599 | dc5bf3f40ad3 |
| child 6617 | 2d56911d7329 |
--- a/doc-src/Intro/Makefile Thu May 06 18:48:46 1999 +0200 +++ b/doc-src/Intro/Makefile Thu May 06 19:04:20 1999 +0200 @@ -26,3 +26,16 @@ $(LATEX) $(NAME) $(SEDINDEX) $(NAME) $(LATEX) $(NAME) + + +pdf: $(NAME).pdf + +$(NAME).pdf: $(FILES) isabelle.png + touch $(NAME).ind + $(PDFLATEX) $(NAME) + $(BIBTEX) $(NAME) + $(PDFLATEX) $(NAME) + $(PDFLATEX) $(NAME) + $(SEDINDEX) $(NAME) + $(FIXBOOKMARKS) $(NAME).out + $(PDFLATEX) $(NAME)