--- 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 "$?"
--- 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)