tuned dist version;
authorwenzelm
Thu, 28 May 1998 14:50:40 +0200
changeset 4982 6f96354267e0
parent 4981 9703ba0e9122
child 4983 2c567fcdb36d
tuned dist version;
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