1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/Tools/install	Mon Aug 24 15:49:53 1998 +0200
     1.3 @@ -0,0 +1,53 @@
     1.4 +#!/bin/bash
     1.5 +#
     1.6 +# $Id$
     1.7 +#
     1.8 +# DESCRIPTION: install binaries with absolute references to ISABELLE_HOME/bin
     1.9 +
    1.10 +
    1.11 +PRG=$(basename $0)
    1.12 +
    1.13 +function usage()
    1.14 +{
    1.15 +  echo
    1.16 +  echo "Usage: $PRG DIR"
    1.17 +  echo
    1.18 +  echo "  Install binaries in directory DIR with absolute references to"
    1.19 +  echo "  $ISABELLE_HOME/bin (non-movable)."
    1.20 +  echo
    1.21 +  exit 1
    1.22 +}
    1.23 +
    1.24 +function fail()
    1.25 +{
    1.26 +  echo "$1" >&2
    1.27 +  exit 2
    1.28 +}
    1.29 +
    1.30 +
    1.31 +## args
    1.32 +
    1.33 +DIR=""
    1.34 +[ $# -ge 1 ] && { DIR="$1"; shift; }
    1.35 +
    1.36 +[ $# -ne 0 -o -z "$DIR" -o "$DIR" = "-?" ] && usage
    1.37 +
    1.38 +
    1.39 +## main
    1.40 +
    1.41 +[ ! -d "$DIR" ] && fail "Bad directory: $DIR"
    1.42 +
    1.43 +BASH=$(type -path bash)
    1.44 +[ -z "$BASH" ] && fail "Cannot find bash!"
    1.45 +
    1.46 +for BIN in $ISABELLE_HOME/bin/*
    1.47 +do
    1.48 +  if [ -f "$BIN" -a -x "$BIN" ]; then
    1.49 +    B=$DIR/$(basename $BIN)
    1.50 +    echo "install $B"
    1.51 +    echo "#!$BASH" >$B || fail "Cannot write file: $B"
    1.52 +    echo >>$B
    1.53 +    echo "$BIN \"\$@\"" >>$B
    1.54 +    chmod +x $B
    1.55 +  fi
    1.56 +done