lib/Tools/install

-d DISTDIR;
tuned;

#!/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 binaries in directory BINDIR with absolute references to"
  echo "  DISTDIR/bin, which basically 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
    h)
      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