doc-src/System/Makefile
changeset 6623 021728c71030
parent 6601 51eed1aefccd
child 6629 6edc66a9d80b
     1.1 --- a/doc-src/System/Makefile	Mon May 10 15:35:03 1999 +0200
     1.2 +++ b/doc-src/System/Makefile	Mon May 10 16:35:22 1999 +0200
     1.3 @@ -24,3 +24,12 @@
     1.4  	$(LATEX) $(NAME)
     1.5  	$(SEDINDEX) $(NAME)
     1.6  	$(LATEX) $(NAME)
     1.7 +
     1.8 +pdf: $(NAME).pdf
     1.9 +
    1.10 +$(NAME).pdf: $(FILES) isabelle.pdf
    1.11 +	touch $(NAME).ind
    1.12 +	$(PDFLATEX) $(NAME)
    1.13 +	$(PDFLATEX) $(NAME)
    1.14 +	$(SEDINDEX) $(NAME)
    1.15 +	$(PDFLATEX) $(NAME)