# HG changeset patch
# User wenzelm
# Date 896359840 -7200
# Node ID 6f96354267e0810fbb84421df64636b14fa0bf8b
# Parent  9703ba0e912258865a91ae7200393b708dac1159
tuned dist version;

diff -r 9703ba0e9122 -r 6f96354267e0 Admin/makedist
--- a/Admin/makedist	Thu May 28 12:24:05 1998 +0200
+++ b/Admin/makedist	Thu May 28 14:50:40 1998 +0200
@@ -80,10 +80,12 @@
 
 if [ "$VERSION" = "-" ]; then
   DISTNAME=Isabelle_$DATE
+  DISTVERSION="$DISTNAME"
   EXPORT="checkout -P"
   UNOFFICIAL=true
 else
   DISTNAME="$VERSION"
+  DISTVERSION="$DISTNAME: $DISTDATE"
   EXPORT="export -r $VERSION"
   UNOFFICIAL=""
 fi
@@ -147,8 +149,8 @@
   } >UNOFFICIAL
 fi
 
-perl -pi -e "s/Internal working version of Isabelle/$DISTNAME: $DISTDATE/" src/Pure/ROOT.ML
-perl -pi -e "s/an internal working version of Isabelle/$DISTNAME: $DISTDATE/" README.html
+perl -pi -e "s/Internal working version of Isabelle/$DISTVERSION/" src/Pure/ROOT.ML
+perl -pi -e "s/an internal working version of Isabelle/$DISTVERSION/" README.html
 lynx -dump README.html >README