changed for new naming style of HTML files (leading ".")
authorclasohm
Tue, 07 Nov 1995 13:15:43 +0100
changeset 1324 113785b2929b
parent 1323 ae24fa249266
child 1325 32f6d6920204
changed for new naming style of HTML files (leading ".")
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