lib/Tools/install

better miniscoping rules: the premise C~={} is not good
because Safe_tac eliminates such assumptions.

#!/bin/bash
#
# $Id$
#
# DESCRIPTION: install binaries with absolute references to distribution


PRG=$(basename $0)

function usage()
{
  echo
  echo "Usage: $PRG BINDIR"
  echo
  echo "  Options are:"
  echo "    -d DISTDIR   use DISTDIR as Isabelle distribution (default ISABELLE_HOME)"
  echo
  echo "  Install standalone Isabelle binaries in directory BINDIR with absolute"
  echo "  references to DISTDIR/bin, which becomes non-relocatable this way."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

DISTDIR="$ISABELLE_HOME"

while getopts "d:" OPT
do
  case "$OPT" in
    d)
      DISTDIR="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

BINDIR=""
[ $# -ge 1 ] && { BINDIR="$1"; shift; }

[ $# -ne 0 -o -z "$BINDIR" -o "$BINDIR" = "-?" ] && usage


## main

mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"

BASH=$(type -path bash)
[ -z "$BASH" ] && fail "Cannot find bash!"

echo "using $DISTDIR"

for NAME in isatool isabelle Isabelle
do
  BIN="$BINDIR/$NAME"
  DIST="$DISTDIR/bin/$NAME"
  echo "installing $BIN"
  echo "#!$BASH" >$BIN || fail "Cannot write file: $BIN"
  echo >>$BIN
  echo "exec $DIST \"\$@\"" >>$BIN
  chmod +x $BIN
done