lib/scripts/getsettings
changeset 47490 f4348634595b
parent 47465 71d5f37ee2bf
child 47525 9c8a1b9c0630
equal deleted inserted replaced
47489:04e7d09ade7a 47490:f4348634595b
    95 
    95 
    96 #robust invocation via ISABELLE_JDK_HOME
    96 #robust invocation via ISABELLE_JDK_HOME
    97 function isabelle_jdk () {
    97 function isabelle_jdk () {
    98   if [ -z "$ISABELLE_JDK_HOME" ]; then
    98   if [ -z "$ISABELLE_JDK_HOME" ]; then
    99     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
    99     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
   100     return 2
   100     return 127
   101   else
   101   else
   102     local PRG="$1"; shift
   102     local PRG="$1"; shift
   103     "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
   103     "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
   104   fi
   104   fi
   105 }
   105 }
   106 
   106 
   107 #robust invocation via SCALA_HOME
   107 #robust invocation via SCALA_HOME
   108 function isabelle_scala () {
   108 function isabelle_scala () {
   109   if [ -z "$ISABELLE_JDK_HOME" ]; then
   109   if [ -z "$ISABELLE_JDK_HOME" ]; then
   110     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
   110     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
   111     return 2
   111     return 127
   112   elif [ -z "$SCALA_HOME" ]; then
   112   elif [ -z "$SCALA_HOME" ]; then
   113     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
   113     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
   114     return 2
   114     return 127
   115   else
   115   else
   116     local PRG="$1"; shift
   116     local PRG="$1"; shift
   117     "$SCALA_HOME/bin/$PRG" "$@"
   117     "$SCALA_HOME/bin/$PRG" "$@"
   118   fi
   118   fi
   119 }
   119 }