# HG changeset patch
# User wenzelm
# Date 1216318512 -7200
# Node ID 9df10b28aa60f1dd365d0f4f65f3401624a21ac2
# Parent  83e6a4c43d17da913893181d07d563a3db1f89d8
structure Distribution: swapped default for is_official;
removed obsolete (?) sync/sleep;

diff -r 83e6a4c43d17 -r 9df10b28aa60 Admin/makedist
--- a/Admin/makedist	Thu Jul 17 20:05:19 2008 +0200
+++ b/Admin/makedist	Thu Jul 17 20:15:12 2008 +0200
@@ -162,7 +162,8 @@
     echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
     echo
   } >ANNOUNCE
-  perl -pi -e "s/val is_official = true/val is_official = false/" src/Pure/ROOT.ML
+else
+  perl -pi -e "s/val is_official = false/val is_official = true/" src/Pure/ROOT.ML
 fi
 
 perl -pi -e "s/ISABELLE_IDENTIFIER=\"\"/ISABELLE_IDENTIFIER=\"$DISTNAME\"/g;" lib/scripts/getsettings
@@ -195,8 +196,6 @@
 mkdir -p "pdf/$DISTNAME/doc"
 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
 
-sync; sleep 3
-
 echo "$DISTNAME.tar.gz"
 tar cf "$DISTNAME.tar" Isabelle "$DISTNAME"
 gzip "$DISTNAME.tar"
@@ -225,8 +224,6 @@
 rm -rf "${DISTNAME}-old"
 
 
-# final note
-
 echo "###"
 echo "### Finished makedist."
 echo "###"