commented out chwon, chmod;
authorwenzelm
Fri, 07 Mar 1997 16:40:30 +0100
changeset 2776 7e99c2cbfb24
parent 2775 7a4989d685d6
child 2777 3396eb1fa01d
commented out chwon, chmod;
Admin/makedist
--- a/Admin/makedist	Fri Mar 07 16:16:47 1997 +0100
+++ b/Admin/makedist	Fri Mar 07 16:40:30 1997 +0100
@@ -142,9 +142,10 @@
 
 cd $DISTBASE
 
-chown -R $LOGNAME:isabelle $DISTNAME
-chmod -R u+w $DISTNAME
-chmod -R g-w $DISTNAME
+#FIXME doesn't work!?
+#chown -R $LOGNAME:isabelle $DISTNAME
+#chmod -R u+w $DISTNAME
+#chmod -R g-w $DISTNAME
 
 tar cf - $DISTNAME | gzip >$DISTNAME.tar.gz