# HG changeset patch
# User wenzelm
# Date 858591597 -3600
# Node ID 2d259a41cd77b3871f4acd814158866c0a070ccb
# Parent  b30c41754c862d86f25017cae69d458d34955338
uncommented chown / chmod (again);

diff -r b30c41754c86 -r 2d259a41cd77 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