Admin/makedist
changeset 2776 7e99c2cbfb24
parent 2686 351c45bb338d
child 2794 2d259a41cd77
--- 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