lib/Tools/install
author wenzelm
Mon Aug 24 15:49:53 1998 +0200 (1998-08-24)
changeset 5362 29ce4f1fe72c
child 5367 33f81e980c93
permissions -rwxr-xr-x
install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm@5362
     1
#!/bin/bash
wenzelm@5362
     2
#
wenzelm@5362
     3
# $Id$
wenzelm@5362
     4
#
wenzelm@5362
     5
# DESCRIPTION: install binaries with absolute references to ISABELLE_HOME/bin
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@5362
    13
  echo "Usage: $PRG DIR"
wenzelm@5362
    14
  echo
wenzelm@5362
    15
  echo "  Install binaries in directory DIR with absolute references to"
wenzelm@5362
    16
  echo "  $ISABELLE_HOME/bin (non-movable)."
wenzelm@5362
    17
  echo
wenzelm@5362
    18
  exit 1
wenzelm@5362
    19
}
wenzelm@5362
    20
wenzelm@5362
    21
function fail()
wenzelm@5362
    22
{
wenzelm@5362
    23
  echo "$1" >&2
wenzelm@5362
    24
  exit 2
wenzelm@5362
    25
}
wenzelm@5362
    26
wenzelm@5362
    27
wenzelm@5362
    28
## args
wenzelm@5362
    29
wenzelm@5362
    30
DIR=""
wenzelm@5362
    31
[ $# -ge 1 ] && { DIR="$1"; shift; }
wenzelm@5362
    32
wenzelm@5362
    33
[ $# -ne 0 -o -z "$DIR" -o "$DIR" = "-?" ] && usage
wenzelm@5362
    34
wenzelm@5362
    35
wenzelm@5362
    36
## main
wenzelm@5362
    37
wenzelm@5362
    38
[ ! -d "$DIR" ] && fail "Bad directory: $DIR"
wenzelm@5362
    39
wenzelm@5362
    40
BASH=$(type -path bash)
wenzelm@5362
    41
[ -z "$BASH" ] && fail "Cannot find bash!"
wenzelm@5362
    42
wenzelm@5362
    43
for BIN in $ISABELLE_HOME/bin/*
wenzelm@5362
    44
do
wenzelm@5362
    45
  if [ -f "$BIN" -a -x "$BIN" ]; then
wenzelm@5362
    46
    B=$DIR/$(basename $BIN)
wenzelm@5362
    47
    echo "install $B"
wenzelm@5362
    48
    echo "#!$BASH" >$B || fail "Cannot write file: $B"
wenzelm@5362
    49
    echo >>$B
wenzelm@5362
    50
    echo "$BIN \"\$@\"" >>$B
wenzelm@5362
    51
    chmod +x $B
wenzelm@5362
    52
  fi
wenzelm@5362
    53
done