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