# HG changeset patch
# User clasohm
# Date 815746543 -3600
# Node ID 113785b2929bb8f312ff8cfa8b27877b00ce5deb
# Parent  ae24fa2492669949bd30b80b14c2fd2a080eacad
changed for new naming style of HTML files (leading ".")

diff -r ae24fa249266 -r 113785b2929b src/Tools/rm_html.sh
--- a/src/Tools/rm_html.sh	Tue Nov 07 13:15:04 1995 +0100
+++ b/src/Tools/rm_html.sh	Tue Nov 07 13:15:43 1995 +0100
@@ -2,9 +2,4 @@
 # Executed from the main Isabelle directory, this script removes all files
 # made when Isabelle was used with set MAKE_HTML
 
-rm */theory_list.txt */index.html */Pure_sub.html */CPure_sub.html
-foreach f (*/*.thy */*/*.thy */*/*/*.thy)
-  if (-f $f:r.html) then
-    rm $f:r.html $f:r_sub.html $f:r_sup.html
-  endif
-end
+rm */.theory_list.txt */index.html */.*.html */*/.*.html */*/*/.*.html