added local index.html files to rm_html.sh;
authorclasohm
Tue, 21 Nov 1995 12:40:04 +0100
changeset 1349 ef26adb4e5b6
parent 1348 b9305143fa91
child 1350 5bf4a54ba25f
added local index.html files to rm_html.sh; replaced www4 by hpbroy12 in install_html.sh because of login problems on www4
src/Tools/install_html.sh
src/Tools/rm_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
--- 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