lib/Tools/install
changeset 50132 180d086c30dd
parent 29143 72c960b2b83e
child 52116 abf9fcfa65cf
     1.1 --- a/lib/Tools/install	Tue Nov 20 14:55:52 2012 +0100
     1.2 +++ b/lib/Tools/install	Tue Nov 20 15:18:11 2012 +0100
     1.3 @@ -10,14 +10,13 @@
     1.4  function usage()
     1.5  {
     1.6    echo
     1.7 -  echo "Usage: isabelle $PRG [OPTIONS]"
     1.8 +  echo "Usage: isabelle $PRG [OPTIONS] BINDIR"
     1.9    echo
    1.10    echo "  Options are:"
    1.11    echo "    -d DISTDIR   refer to DISTDIR as Isabelle distribution"
    1.12    echo "                 (default ISABELLE_HOME)"
    1.13 -  echo "    -p DIR       install standalone binaries in DIR"
    1.14    echo
    1.15 -  echo "  Install Isabelle executables with absolute references to the current"
    1.16 +  echo "  Install Isabelle executables with absolute references to the"
    1.17    echo "  distribution directory."
    1.18    echo
    1.19    exit 1
    1.20 @@ -34,21 +33,15 @@
    1.21  
    1.22  # options
    1.23  
    1.24 -NO_OPTS=true
    1.25 -
    1.26  DISTDIR="$ISABELLE_HOME"
    1.27  BINDIR=""
    1.28  
    1.29 -while getopts "d:p:" OPT
    1.30 +while getopts "d:" OPT
    1.31  do
    1.32 -  NO_OPTS=""
    1.33    case "$OPT" in
    1.34      d)
    1.35        DISTDIR="$OPTARG"
    1.36        ;;
    1.37 -    p)
    1.38 -      BINDIR="$OPTARG"
    1.39 -      ;;
    1.40      \?)
    1.41        usage
    1.42        ;;
    1.43 @@ -60,28 +53,25 @@
    1.44  
    1.45  # args
    1.46  
    1.47 -[ "$#" -ne 0 -o -n "$NO_OPTS" ] && usage
    1.48 +[ "$#" -ge 1 ] && { BINDIR="$1"; shift; }
    1.49 +[ "$#" -ne 0 -o -z "$BINDIR" ] && usage
    1.50  
    1.51  
    1.52  ## main
    1.53  
    1.54 -echo "referring to distribution at $DISTDIR"
    1.55 -
    1.56 +echo "referring to distribution at \"$DISTDIR\""
    1.57  
    1.58 -# standalone binaries
    1.59 -
    1.60 -if [ -n "$BINDIR" ]; then
    1.61 -  mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
    1.62 +mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\""
    1.63  
    1.64 -  for NAME in isabelle isabelle-process
    1.65 -  do
    1.66 -    BIN="$BINDIR/$NAME"
    1.67 -    DIST="$DISTDIR/bin/$NAME"
    1.68 -    echo "installing $BIN"
    1.69 -    rm -f "$BIN"
    1.70 -    echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN"
    1.71 -    echo >> "$BIN"
    1.72 -    echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
    1.73 -    chmod +x "$BIN"
    1.74 -  done
    1.75 -fi
    1.76 +for NAME in isabelle isabelle-process
    1.77 +do
    1.78 +  BIN="$BINDIR/$NAME"
    1.79 +  DIST="$DISTDIR/bin/$NAME"
    1.80 +  echo "installing $BIN"
    1.81 +  rm -f "$BIN"
    1.82 +  echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN"
    1.83 +  echo >> "$BIN"
    1.84 +  echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
    1.85 +  chmod +x "$BIN"
    1.86 +done
    1.87 +