lib/Tools/install

 PRG=$(basename "$0")
 
 function usage()
 {
   echo
-  echo "Usage: isabelle $PRG [OPTIONS]"
+  echo "Usage: isabelle $PRG [OPTIONS] BINDIR"
   echo
   echo "  Options are:"
   echo "    -d DISTDIR   refer to DISTDIR as Isabelle distribution"
   echo "                 (default ISABELLE_HOME)"
-  echo "    -p DIR       install standalone binaries in DIR"
   echo
-  echo "  Install Isabelle executables with absolute references to the current"
+  echo "  Install Isabelle executables with absolute references to the"
   echo "  distribution directory."
   echo
   exit 1
 }
 

 
 ## process command line
 
 # options
 
-NO_OPTS=true
-
 DISTDIR="$ISABELLE_HOME"
 BINDIR=""
 
-while getopts "d:p:" OPT
+while getopts "d:" OPT
 do
-  NO_OPTS=""
   case "$OPT" in
     d)
       DISTDIR="$OPTARG"
-      ;;
-    p)
-      BINDIR="$OPTARG"
       ;;
     \?)
       usage
       ;;
   esac

 shift $(($OPTIND - 1))
 
 
 # args
 
-[ "$#" -ne 0 -o -n "$NO_OPTS" ] && usage
+[ "$#" -ge 1 ] && { BINDIR="$1"; shift; }
+[ "$#" -ne 0 -o -z "$BINDIR" ] && usage
 
 
 ## main
 
-echo "referring to distribution at $DISTDIR"
+echo "referring to distribution at \"$DISTDIR\""
 
+mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\""
 
-# standalone binaries
+for NAME in isabelle isabelle-process
+do
+  BIN="$BINDIR/$NAME"
+  DIST="$DISTDIR/bin/$NAME"
+  echo "installing $BIN"
+  rm -f "$BIN"
+  echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN"
+  echo >> "$BIN"
+  echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
+  chmod +x "$BIN"
+done
 
-if [ -n "$BINDIR" ]; then
-  mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
-
-  for NAME in isabelle isabelle-process
-  do
-    BIN="$BINDIR/$NAME"
-    DIST="$DISTDIR/bin/$NAME"
-    echo "installing $BIN"
-    rm -f "$BIN"
-    echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN"
-    echo >> "$BIN"
-    echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
-    chmod +x "$BIN"
-  done
-fi