src/Tools/rm_html.sh
author clasohm
Wed, 13 Dec 1995 14:14:06 +0100
changeset 1403 cdfa3ffcead2
parent 1349 ef26adb4e5b6
permissions -rwxr-xr-x
renamed parents_of to parents_of_name to avoid name clash with function from thm.ML

#!/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