src/Tools/rm_html.sh
author clasohm
Mon, 19 Feb 1996 13:54:15 +0100
changeset 1514 3e262b1c0b6c
parent 1349 ef26adb4e5b6
permissions -rwxr-xr-x
fixed bug in init_data (put was only invoked for the first date)

#!/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 */*/.theory_list.txt */*/*/.theory_list.txt \
   */index.html */*/index.html */*/*/index.html \
   */.*.html */*/.*.html */*/*/.*.html