--- a/Admin/makedist Thu Nov 06 12:27:12 1997 +0100
+++ b/Admin/makedist Thu Nov 06 16:40:45 1997 +0100
@@ -152,7 +152,6 @@
cd $DISTBASE
-#FIXME sometimes doesn't work!?
chown -R $LOGNAME:isabelle $DISTNAME
chmod -R u+w $DISTNAME
chmod -R g+w $DISTNAME