--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Release/build_library Tue Jan 15 12:30:23 2013 +0100
@@ -0,0 +1,96 @@
+#!/usr/bin/env bash
+#
+# build Isabelle HTML library from platform bundle
+
+## diagnostics
+
+PRG=$(basename "$0")
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG [OPTIONS] ARCHIVE"
+ echo
+ echo " Options are:"
+ echo " -j INT maximum number of parallel jobs (default 1)"
+ echo
+ echo " Build Isabelle HTML library from platform bundle."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+# options
+
+JOBS=""
+
+while getopts "j:" OPT
+do
+ case "$OPT" in
+ j)
+ JOBS="-j $OPTARG"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ "$#" -ne 1 ] && usage
+
+ARCHIVE="$1"; shift
+
+[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
+ARCHIVE_BASE="$(basename "$ARCHIVE")"
+ARCHIVE_DIR="$(cd "$(dirname "$ARCHIVE")"; echo "$PWD")"
+ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
+
+
+## main
+
+export COPYFILE_DISABLE=true
+
+TMP="/var/tmp/isabelle-makedist$$"
+mkdir "$TMP" || fail "Cannot create directory: \"$TMP\""
+
+cd "$TMP"
+tar -x -z -f "$ARCHIVE_FULL"
+
+cd *
+ISABELLE_NAME="$(basename "$PWD")"
+
+echo "Z3_NON_COMMERCIAL=yes" >> etc/settings
+echo "ISABELLE_FULL_TEST=true" >> etc/settings
+
+echo -n > src/Doc/ROOT
+
+env ISABELLE_IDENTIFIER="${ISABELLE_NAME}-build" \
+ ./bin/isabelle build $JOBS -s -c -a -o browser_info \
+ -o "document=pdf" -o "document_variants=document:outline=/proof,/ML"
+RC="$?"
+
+cd ..
+
+if [ "$RC" = 0 ]; then
+ chmod -R g=o "$ISABELLE_NAME"
+ tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
+fi
+
+# clean up
+cd /tmp
+rm -rf "$TMP"
+
+exit "$RC"