--- a/Admin/makedist Sat Sep 23 16:12:07 2000 +0200
+++ b/Admin/makedist Mon Sep 25 12:04:10 2000 +0200
@@ -198,6 +198,9 @@
cd "$DISTBASE"
+rm -f Isabelle
+ln -s "$DISTNAME" Isabelle
+
chown -R "$LOGNAME" "$DISTNAME"
chgrp -R isabelle "$DISTNAME"
chmod -R u+w "$DISTNAME"