1.1 --- a/Admin/makedist	Thu Jul 17 20:05:19 2008 +0200
     1.2 +++ b/Admin/makedist	Thu Jul 17 20:15:12 2008 +0200
     1.3 @@ -162,7 +162,8 @@
     1.4      echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
     1.5      echo
     1.6    } >ANNOUNCE
     1.7 -  perl -pi -e "s/val is_official = true/val is_official = false/" src/Pure/ROOT.ML
     1.8 +else
     1.9 +  perl -pi -e "s/val is_official = false/val is_official = true/" src/Pure/ROOT.ML
    1.10  fi
    1.11  
    1.12  perl -pi -e "s/ISABELLE_IDENTIFIER=\"\"/ISABELLE_IDENTIFIER=\"$DISTNAME\"/g;" lib/scripts/getsettings
    1.13 @@ -195,8 +196,6 @@
    1.14  mkdir -p "pdf/$DISTNAME/doc"
    1.15  mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
    1.16  
    1.17 -sync; sleep 3
    1.18 -
    1.19  echo "$DISTNAME.tar.gz"
    1.20  tar cf "$DISTNAME.tar" Isabelle "$DISTNAME"
    1.21  gzip "$DISTNAME.tar"
    1.22 @@ -225,8 +224,6 @@
    1.23  rm -rf "${DISTNAME}-old"
    1.24  
    1.25  
    1.26 -# final note
    1.27 -
    1.28  echo "###"
    1.29  echo "### Finished makedist."
    1.30  echo "###"