# 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/*"