added local index.html files to rm_html.sh;
replaced www4 by hpbroy12 in install_html.sh because of login problems on www4
--- a/src/Tools/install_html.sh Tue Nov 21 12:36:31 1995 +0100
+++ b/src/Tools/install_html.sh Tue Nov 21 12:40:04 1995 +0100
@@ -6,15 +6,15 @@
# the wanted ones as parameters as in "install_html.sh HOL HOLCF".
if ( "$*" == "" ) then
- rsh www4 "rm -r .html-data/isabelle/*; mkdir .html-data/isabelle/Tools"
+ rsh hpbroy12 "rm -r .html-data/isabelle/*; mkdir .html-data/isabelle/Tools"
endif
-rcp index.html www4:.html-data/isabelle
-rcp Tools/*_arrow.gif www4:.html-data/isabelle/Tools
+rcp index.html hpbroy12:.html-data/isabelle
+rcp Tools/*_arrow.gif hpbroy12:.html-data/isabelle/Tools
if ( "$*" == "" ) then
rcp -r CCL CTT Cube FOL FOLP HOL HOLCF LCF LK Modal ZF \
- www4:.html-data/isabelle
+ hpbroy12:.html-data/isabelle
else
- rcp -r $* www4:.html-data/isabelle
+ rcp -r $* hpbroy12:.html-data/isabelle
endif
--- a/src/Tools/rm_html.sh Tue Nov 21 12:36:31 1995 +0100
+++ b/src/Tools/rm_html.sh Tue Nov 21 12:40:04 1995 +0100
@@ -2,4 +2,6 @@
# 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 */.*.html */*/.*.html */*/*/.*.html
+rm */.theory_list.txt */*/.theory_list.txt */*/*/.theory_list.txt \
+ */index.html */*/index.html */*/*/index.html \
+ */.*.html */*/.*.html */*/*/.*.html