uncommented chown / chmod (again);
authorwenzelm
Mon, 17 Mar 1997 10:39:57 +0100
changeset 2794 2d259a41cd77
parent 2793 b30c41754c86
child 2795 d136fff43370
uncommented chown / chmod (again);
Admin/makedist
--- 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