# HG changeset patch
# User clasohm
# Date 816954004 -3600
# Node ID ef26adb4e5b67c62b1e9fee74de8886797b9bac9
# Parent  b9305143fa91e3cec1bd87c0bf9668ddd63da5e4
added local index.html files to rm_html.sh;
replaced www4 by hpbroy12 in install_html.sh because of login problems on www4

diff -r b9305143fa91 -r ef26adb4e5b6 src/Tools/install_html.sh
--- 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
diff -r b9305143fa91 -r ef26adb4e5b6 src/Tools/rm_html.sh
--- 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