lib/scripts/getsettings
changeset 47490 f4348634595b
parent 47465 71d5f37ee2bf
child 47525 9c8a1b9c0630
     1.1 --- a/lib/scripts/getsettings	Mon Apr 16 11:24:57 2012 +0200
     1.2 +++ b/lib/scripts/getsettings	Mon Apr 16 15:09:47 2012 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4  function isabelle_jdk () {
     1.5    if [ -z "$ISABELLE_JDK_HOME" ]; then
     1.6      echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
     1.7 -    return 2
     1.8 +    return 127
     1.9    else
    1.10      local PRG="$1"; shift
    1.11      "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
    1.12 @@ -108,10 +108,10 @@
    1.13  function isabelle_scala () {
    1.14    if [ -z "$ISABELLE_JDK_HOME" ]; then
    1.15      echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
    1.16 -    return 2
    1.17 +    return 127
    1.18    elif [ -z "$SCALA_HOME" ]; then
    1.19      echo "Unknown SCALA_HOME -- Scala unavailable" >&2
    1.20 -    return 2
    1.21 +    return 127
    1.22    else
    1.23      local PRG="$1"; shift
    1.24      "$SCALA_HOME/bin/$PRG" "$@"