lib/scripts/getsettings
changeset 47254 de2fb19683f4
parent 47115 1a05adae1cc9
child 47461 5a7903ba2dac
equal deleted inserted replaced
47253:a00c5c88d8f3 47254:de2fb19683f4
    90 }
    90 }
    91 
    91 
    92 #robust invocation via ISABELLE_JDK_HOME
    92 #robust invocation via ISABELLE_JDK_HOME
    93 function isabelle_jdk () {
    93 function isabelle_jdk () {
    94   [ -z "$ISABELLE_JDK_HOME" ] && \
    94   [ -z "$ISABELLE_JDK_HOME" ] && \
    95     { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable"; exit 2; }
    95     { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2; return 2; }
    96   local PRG="$1"; shift
    96   local PRG="$1"; shift
    97   "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
    97   "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
    98 }
    98 }
    99 
    99 
   100 #robust invocation via SCALA_HOME
   100 #robust invocation via SCALA_HOME
   101 function isabelle_scala () {
   101 function isabelle_scala () {
   102   [ -z "$SCALA_HOME" ] && \
   102   [ -z "$SCALA_HOME" ] && \
   103     { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; }
   103     { echo "Unknown SCALA_HOME -- Scala unavailable" >&2; return 2; }
   104   local PRG="$1"; shift
   104   local PRG="$1"; shift
   105   "$SCALA_HOME/bin/$PRG" "$@"
   105   "$SCALA_HOME/bin/$PRG" "$@"
   106 }
   106 }
   107 
   107 
   108 #CLASSPATH convenience
   108 #CLASSPATH convenience