# HG changeset patch
# User clasohm
# Date 819026636 -3600
# Node ID dc73ca67b5acd9b1934e5a3d9bfa907949b9574f
# Parent  e9ca85a3713c8c12e6c4d495b467791ebc4b0269
added chmod and chgrp

diff -r e9ca85a3713c -r dc73ca67b5ac src/Tools/install_html.sh
--- a/src/Tools/install_html.sh	Fri Dec 15 12:15:39 1995 +0100
+++ b/src/Tools/install_html.sh	Fri Dec 15 12:23:56 1995 +0100
@@ -6,15 +6,19 @@
 # the wanted ones as parameters as in "install_html.sh HOL HOLCF".
 
 if ( "$*" == "" ) then
-  rsh hpbroy12 "rm -r .html-data/isabelle/*; mkdir .html-data/isabelle/Tools"
+  rsh www4 "rm -r .html-data/isabelle/*; mkdir .html-data/isabelle/Tools; \
+            chmod o-w Tools"
 endif
 
-rcp index.html hpbroy12:.html-data/isabelle
-rcp Tools/*_arrow.gif hpbroy12:.html-data/isabelle/Tools
+rcp index.html www4:.html-data/isabelle
+rcp Tools/*_arrow.gif www4:.html-data/isabelle/Tools
 
 if ( "$*" == "" ) then
   rcp -r CCL CTT Cube FOL FOLP HOL HOLCF LCF LK Modal ZF \
-         hpbroy12:.html-data/isabelle
+         www4:.html-data/isabelle
 else
-  rcp -r $* hpbroy12:.html-data/isabelle
+  rcp -r $* www4:.html-data/isabelle
 endif
+rsh www4 "chgrp -R isabelle .html-data/isabelle/*; \
+          chmod -R g+w .html-data/isabelle/*"
+