| changeset 8847 | d6c92979fa51 |
| parent 8828 | 5be2d1745c61 |
| child 9695 | ec7d7f877712 |
--- a/doc-src/TutorialI/Makefile Tue May 09 16:05:30 2000 +0200 +++ b/doc-src/TutorialI/Makefile Tue May 09 16:05:45 2000 +0200 @@ -14,7 +14,7 @@ NAME = tutorial FILES = tutorial.tex basics.tex fp.tex appendix.tex \ ../iman.sty ttbox.sty extra.sty \ - isabelle.sty isabellesym.sty pdfsetup.sty + isabelle.sty isabellesym.sty ../pdfsetup.sty dvi: $(NAME).dvi