remove unnecessary TeX files
authorpaulson
Thu, 03 May 2001 10:27:04 +0200
changeset 11279 aaa0ad8fea6b
parent 11278 9710486b886b
child 11280 6fdc4c4ccec1
remove unnecessary TeX files
doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Wed May 02 11:54:18 2001 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Thu May 03 10:27:04 2001 +0200
@@ -36,6 +36,8 @@
 	@rm -f */document/isabellesym.sty
 	@rm -f */document/pdfsetup.sty
 	@rm -f */document/session.tex
+	@rm -f Rules/document/*.tex
+	@rm -f Sets/document/*.tex
 
 
 ## HOL-Ifexpr