Admin/makedist
changeset 2794 2d259a41cd77
parent 2776 7e99c2cbfb24
child 2829 c6b491e837cb
--- a/Admin/makedist	Fri Mar 14 10:37:01 1997 +0100
+++ b/Admin/makedist	Mon Mar 17 10:39:57 1997 +0100
@@ -142,10 +142,10 @@
 
 cd $DISTBASE
 
-#FIXME doesn't work!?
-#chown -R $LOGNAME:isabelle $DISTNAME
-#chmod -R u+w $DISTNAME
-#chmod -R g-w $DISTNAME
+#FIXME sometimes 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