lib/Tools/install
author wenzelm
Tue Oct 21 20:18:07 2008 +0200 (2008-10-21)
changeset 28650 a7ba12e0d3b7
parent 28504 7ad7d7d6df47
child 28915 0642cbb60c98
permissions -rwxr-xr-x
tuned usage line;
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 #
     6 # DESCRIPTION: install standalone Isabelle executables
     7 
     8 
     9 PRG=$(basename "$0")
    10 
    11 function usage()
    12 {
    13   echo
    14   echo "Usage: isabelle $PRG [OPTIONS]"
    15   echo
    16   echo "  Options are:"
    17   echo "    -d DISTDIR   refer to DISTDIR as Isabelle distribution"
    18   echo "                 (default ISABELLE_HOME)"
    19   echo "    -p DIR       install standalone binaries in DIR"
    20   echo
    21   echo "  Install Isabelle executables with absolute references to the current"
    22   echo "  distribution directory."
    23   echo
    24   exit 1
    25 }
    26 
    27 function fail()
    28 {
    29   echo "$1" >&2
    30   exit 2
    31 }
    32 
    33 
    34 ## process command line
    35 
    36 # options
    37 
    38 NO_OPTS=true
    39 
    40 DISTDIR="$ISABELLE_HOME"
    41 BINDIR=""
    42 
    43 while getopts "d:p:" OPT
    44 do
    45   NO_OPTS=""
    46   case "$OPT" in
    47     d)
    48       DISTDIR="$OPTARG"
    49       ;;
    50     p)
    51       BINDIR="$OPTARG"
    52       ;;
    53     \?)
    54       usage
    55       ;;
    56   esac
    57 done
    58 
    59 shift $(($OPTIND - 1))
    60 
    61 
    62 # args
    63 
    64 [ "$#" -ne 0 -o -n "$NO_OPTS" ] && usage
    65 
    66 
    67 ## main
    68 
    69 echo "referring to distribution at $DISTDIR"
    70 
    71 
    72 # standalone binaries
    73 
    74 if [ -n "$BINDIR" ]; then
    75   mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
    76 
    77   for NAME in isabelle isabelle-process isabelle-interface
    78   do
    79     BIN="$BINDIR/$NAME"
    80     DIST="$DISTDIR/bin/$NAME"
    81     echo "installing $BIN"
    82     rm -f "$BIN"
    83     echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN"
    84     echo >> "$BIN"
    85     echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
    86     chmod +x "$BIN"
    87   done
    88 fi