diff -r 5245fa2ca8d3 -r 4dc7edfb0b5f Admin/makedist
--- 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