# HG changeset patch
# User wenzelm
# Date 857749230 -3600
# Node ID 7e99c2cbfb245e1615a70a9a83fcd0c8021b648c
# Parent  7a4989d685d6fd309a6f335ac2ccaa2d68e4ac97
commented out chwon, chmod;

diff -r 7a4989d685d6 -r 7e99c2cbfb24 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