# HG changeset patch # User wenzelm # Date 1010168369 -3600 # Node ID fcff0c66b4f450842271725590f3a7d6db2299cd # Parent 425ca8613a1d1b9a38ac902a5872972b149a98fa link Types/typedef images; diff -r 425ca8613a1d -r fcff0c66b4f4 doc-src/TutorialI/Makefile --- a/doc-src/TutorialI/Makefile Thu Jan 03 17:57:04 2002 +0100 +++ b/doc-src/TutorialI/Makefile Fri Jan 04 19:19:29 2002 +0100 @@ -29,6 +29,7 @@ dvi: $(NAME).dvi $(NAME).dvi: $(FILES) isabelle_hol.eps + @ln -sf Types/typedef.eps . $(LATEX) $(NAME) $(BIBTEX) $(NAME) $(LATEX) $(NAME) @@ -39,6 +40,7 @@ pdf: $(NAME).pdf $(NAME).pdf: $(FILES) isabelle_hol.pdf + @ln -sf Types/typedef.pdf . $(PDFLATEX) $(NAME) $(BIBTEX) $(NAME) $(PDFLATEX) $(NAME)