--- a/Admin/makedist Tue Sep 26 17:34:33 2000 +0200 +++ b/Admin/makedist Tue Sep 26 18:09:38 2000 +0200 @@ -201,6 +201,8 @@ cd "$DISTBASE" +echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST + rm -f Isabelle ln -s "$DISTNAME" Isabelle