changeset 9695 | ec7d7f877712 |
parent 8847 | d6c92979fa51 |
child 11400 | ddcfdc38090d |
--- a/doc-src/TutorialI/Makefile Mon Aug 28 13:50:24 2000 +0200 +++ b/doc-src/TutorialI/Makefile Mon Aug 28 13:52:38 2000 +0200 @@ -13,7 +13,7 @@ NAME = tutorial FILES = tutorial.tex basics.tex fp.tex appendix.tex \ - ../iman.sty ttbox.sty extra.sty \ + ../iman.sty ../ttbox.sty ../extra.sty \ isabelle.sty isabellesym.sty ../pdfsetup.sty dvi: $(NAME).dvi