--- a/Admin/Release/build_library Thu Oct 20 11:04:38 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,93 +0,0 @@
-#!/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
-
-#GNU tar (notably on Mac OS X)
-type -p gnutar >/dev/null && function tar() { gnutar "$@"; }
-
-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")"
-
-env ISABELLE_IDENTIFIER="${ISABELLE_NAME}-build" \
- ./bin/isabelle build $JOBS -s -c -a -d '~~/src/Benchmarks' -o browser_info \
- -o "document=pdf" -o "document_variants=document:outline=/proof,/ML"
-RC="$?"
-
-cd ..
-
-if [ "$RC" = 0 ]; then
- chmod -R a+r "$ISABELLE_NAME"
- 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"