diff -r 2f0df5b390e8 -r fcc8b47e4c49 Admin/makedist
--- 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