# HG changeset patch
# User clasohm
# Date 814712553 -3600
# Node ID e9a3287e7387ac184af7a89d0ca92fcd2cd27883
# Parent  9fb65f3db3198746c51a29a4cb1403fdc5154a7d
script for removal of HTML files

diff -r 9fb65f3db319 -r e9a3287e7387 src/Tools/rm_html.sh
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/rm_html.sh	Thu Oct 26 14:02:33 1995 +0100
@@ -0,0 +1,10 @@
+#!/bin/csh
+# 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