# HG changeset patch
# User clasohm
# Date 823172923 -3600
# Node ID fb9ccf06dfe84ee5b513064e757cf63ae2f58df6
# Parent  dcac709dcdd973f915d976d06e4be3f4f673e317
fixed two little bugs

diff -r dcac709dcdd9 -r fb9ccf06dfe8 src/Tools/install_html.sh
--- a/src/Tools/install_html.sh	Wed Jan 31 17:15:03 1996 +0100
+++ b/src/Tools/install_html.sh	Thu Feb 01 12:08:43 1996 +0100
@@ -7,7 +7,7 @@
 
 if ( "$*" == "" ) then
   rsh www4 "rm -r .html-data/isabelle/*; mkdir .html-data/isabelle/Tools; \
-            chmod o-w Tools"
+            chmod og-w .html-data/isabelle/Tools"
 endif
 
 rcp index.html www4:.html-data/isabelle
@@ -19,6 +19,4 @@
 else
   rcp -r $* www4:.html-data/isabelle
 endif
-rsh www4 "chgrp -R isabelle .html-data/isabelle/*; \
-          chmod -R g+w .html-data/isabelle/*"
-
+rsh www4 "chgrp -R isabelle .html-data/isabelle/*;                                       chmod -R g+w .html-data/isabelle/*"