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