# HG changeset patch
# User wenzelm
# Date 1406300308 -7200
# Node ID 34ec8a580917748a177d0201b01f5499f9a8b402
# Parent  38338e759f2608bc7c8e70a3d12728d05051884a
proper option -O;

diff -r 38338e759f26 -r 34ec8a580917 Admin/Release/build
--- a/Admin/Release/build	Fri Jul 25 16:50:49 2014 +0200
+++ b/Admin/Release/build	Fri Jul 25 16:58:28 2014 +0200
@@ -18,6 +18,7 @@
   echo "Usage: isabelle $PRG [OPTIONS] DIR [VERSION]"
   echo
   echo "  Options are:"
+  echo "    -O           official release (not release-candidate)"
   echo "    -j INT       maximum number of parallel jobs (default 1)"
   echo "    -l           build library"
   echo "    -r RELEASE   proper release with name"
@@ -46,13 +47,17 @@
 
 # options
 
+OFFICIAL_RELEASE=""
 JOBS=""
 LIBRARY=""
 RELEASE=""
 
-while getopts "j:lr:" OPT
+while getopts "Oj:lr:" OPT
 do
   case "$OPT" in
+    O)
+      OFFICIAL_RELEASE="-O"
+      ;;
     j)
       check_number "$OPTARG"
       JOBS="-j $OPTARG"
@@ -98,10 +103,10 @@
 
 if [ -z "$RELEASE" ]; then
   DISTNAME="Isabelle_$(env LC_ALL=C date "+%d-%b-%Y")"
-  "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS
+  "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS $OFFICIAL_RELEASE
 else
   DISTNAME="$RELEASE"
-  "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS -r "$RELEASE"
+  "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS $OFFICIAL_RELEASE -r "$RELEASE"
 fi
 [ "$?" = 0 ] || exit "$?"
 
diff -r 38338e759f26 -r 34ec8a580917 Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Fri Jul 25 16:50:49 2014 +0200
+++ b/Admin/lib/Tools/makedist	Fri Jul 25 16:58:28 2014 +0200
@@ -58,7 +58,7 @@
 JOBS=""
 RELEASE=""
 
-while getopts "d:j:r:" OPT
+while getopts "Od:j:r:" OPT
 do
   case "$OPT" in
     O)