# HG changeset patch
# User paulson
# Date 994841418 -7200
# Node ID 26cbf43d76af30d0b9704835f2f9088f138ec6f6
# Parent  ddcfdc38090d391c3536fae127236696d3e1052b
do not remove Rules and Sets TeX files

diff -r ddcfdc38090d -r 26cbf43d76af doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Mon Jul 09 13:43:02 2001 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Wed Jul 11 10:50:18 2001 +0200
@@ -36,8 +36,7 @@
 	@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