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