--- 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