lib/Tools/install
author wenzelm
Fri Aug 28 14:18:46 1998 +0200 (1998-08-28)
changeset 5404 fde117f1006b
parent 5403 aa04ac8bfeae
child 6082 590f9e3bf4d8
permissions -rwxr-xr-x
tuned;
wenzelm@5362
     1
#!/bin/bash
wenzelm@5362
     2
#
wenzelm@5362
     3
# $Id$
wenzelm@5362
     4
#
wenzelm@5403
     5
# DESCRIPTION: install binaries with absolute references to distribution
wenzelm@5362
     6
wenzelm@5362
     7
wenzelm@5362
     8
PRG=$(basename $0)
wenzelm@5362
     9
wenzelm@5362
    10
function usage()
wenzelm@5362
    11
{
wenzelm@5362
    12
  echo
wenzelm@5403
    13
  echo "Usage: $PRG BINDIR"
wenzelm@5362
    14
  echo
wenzelm@5403
    15
  echo "  Options are:"
wenzelm@5403
    16
  echo "    -d DISTDIR   use DISTDIR as Isabelle distribution (default ISABELLE_HOME)"
wenzelm@5403
    17
  echo
wenzelm@5404
    18
  echo "  Install standalone Isabelle binaries in directory BINDIR with absolute"
wenzelm@5404
    19
  echo "  references to DISTDIR/bin, which becomes non-relocatable this way."
wenzelm@5362
    20
  echo
wenzelm@5362
    21
  exit 1
wenzelm@5362
    22
}
wenzelm@5362
    23
wenzelm@5362
    24
function fail()
wenzelm@5362
    25
{
wenzelm@5362
    26
  echo "$1" >&2
wenzelm@5362
    27
  exit 2
wenzelm@5362
    28
}
wenzelm@5362
    29
wenzelm@5362
    30
wenzelm@5403
    31
## process command line
wenzelm@5403
    32
wenzelm@5403
    33
# options
wenzelm@5403
    34
wenzelm@5403
    35
DISTDIR="$ISABELLE_HOME"
wenzelm@5362
    36
wenzelm@5403
    37
while getopts "d:" OPT
wenzelm@5403
    38
do
wenzelm@5403
    39
  case "$OPT" in
wenzelm@5404
    40
    d)
wenzelm@5403
    41
      DISTDIR="$OPTARG"
wenzelm@5403
    42
      ;;
wenzelm@5403
    43
    \?)
wenzelm@5403
    44
      usage
wenzelm@5403
    45
      ;;
wenzelm@5403
    46
  esac
wenzelm@5403
    47
done
wenzelm@5362
    48
wenzelm@5403
    49
shift $(($OPTIND - 1))
wenzelm@5403
    50
wenzelm@5403
    51
wenzelm@5403
    52
# args
wenzelm@5403
    53
wenzelm@5403
    54
BINDIR=""
wenzelm@5403
    55
[ $# -ge 1 ] && { BINDIR="$1"; shift; }
wenzelm@5403
    56
wenzelm@5403
    57
[ $# -ne 0 -o -z "$BINDIR" -o "$BINDIR" = "-?" ] && usage
wenzelm@5362
    58
wenzelm@5362
    59
wenzelm@5362
    60
## main
wenzelm@5362
    61
wenzelm@5403
    62
mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
wenzelm@5362
    63
wenzelm@5362
    64
BASH=$(type -path bash)
wenzelm@5362
    65
[ -z "$BASH" ] && fail "Cannot find bash!"
wenzelm@5362
    66
wenzelm@5403
    67
echo "using $DISTDIR"
wenzelm@5403
    68
wenzelm@5403
    69
for NAME in isatool isabelle Isabelle
wenzelm@5362
    70
do
wenzelm@5403
    71
  BIN="$BINDIR/$NAME"
wenzelm@5403
    72
  DIST="$DISTDIR/bin/$NAME"
wenzelm@5403
    73
  echo "installing $BIN"
wenzelm@5403
    74
  echo "#!$BASH" >$BIN || fail "Cannot write file: $BIN"
wenzelm@5403
    75
  echo >>$BIN
wenzelm@5403
    76
  echo "exec $DIST \"\$@\"" >>$BIN
wenzelm@5403
    77
  chmod +x $BIN
wenzelm@5362
    78
done