diff -r ed0add6f69a7 -r 7f745e4b7cce Admin/makedist
--- a/Admin/makedist	Fri Nov 26 14:19:16 2010 +0100
+++ b/Admin/makedist	Fri Nov 26 14:40:33 2010 +0100
@@ -186,16 +186,13 @@
 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
 echo "$IDENT" >../ISABELLE_IDENT
 
-rm -f Isabelle
-ln -s "$DISTNAME" Isabelle
-
 chown -R "$LOGNAME" "$DISTNAME"
 chmod -R u+w "$DISTNAME"
 chmod -R g=o "$DISTNAME"
-chgrp -R isabelle "$DISTNAME" Isabelle
+chgrp -R isabelle "$DISTNAME"
 
 echo "$DISTNAME.tar.gz"
-tar -czf "$DISTNAME.tar.gz" Isabelle "$DISTNAME"
+tar -czf "$DISTNAME.tar.gz" "$DISTNAME"
 
 
 # cleanup dist