tuned dist version;
authorwenzelm
Thu May 28 14:50:40 1998 +0200 (1998-05-28)
changeset 49826f96354267e0
parent 4981 9703ba0e9122
child 4983 2c567fcdb36d
tuned dist version;
Admin/makedist
     1.1 --- a/Admin/makedist	Thu May 28 12:24:05 1998 +0200
     1.2 +++ b/Admin/makedist	Thu May 28 14:50:40 1998 +0200
     1.3 @@ -80,10 +80,12 @@
     1.4  
     1.5  if [ "$VERSION" = "-" ]; then
     1.6    DISTNAME=Isabelle_$DATE
     1.7 +  DISTVERSION="$DISTNAME"
     1.8    EXPORT="checkout -P"
     1.9    UNOFFICIAL=true
    1.10  else
    1.11    DISTNAME="$VERSION"
    1.12 +  DISTVERSION="$DISTNAME: $DISTDATE"
    1.13    EXPORT="export -r $VERSION"
    1.14    UNOFFICIAL=""
    1.15  fi
    1.16 @@ -147,8 +149,8 @@
    1.17    } >UNOFFICIAL
    1.18  fi
    1.19  
    1.20 -perl -pi -e "s/Internal working version of Isabelle/$DISTNAME: $DISTDATE/" src/Pure/ROOT.ML
    1.21 -perl -pi -e "s/an internal working version of Isabelle/$DISTNAME: $DISTDATE/" README.html
    1.22 +perl -pi -e "s/Internal working version of Isabelle/$DISTVERSION/" src/Pure/ROOT.ML
    1.23 +perl -pi -e "s/an internal working version of Isabelle/$DISTVERSION/" README.html
    1.24  lynx -dump README.html >README
    1.25  
    1.26