diff -r 04e7d09ade7a -r f4348634595b lib/scripts/getsettings
--- a/lib/scripts/getsettings	Mon Apr 16 11:24:57 2012 +0200
+++ b/lib/scripts/getsettings	Mon Apr 16 15:09:47 2012 +0200
@@ -97,7 +97,7 @@
 function isabelle_jdk () {
   if [ -z "$ISABELLE_JDK_HOME" ]; then
     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
-    return 2
+    return 127
   else
     local PRG="$1"; shift
     "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
@@ -108,10 +108,10 @@
 function isabelle_scala () {
   if [ -z "$ISABELLE_JDK_HOME" ]; then
     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
-    return 2
+    return 127
   elif [ -z "$SCALA_HOME" ]; then
     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
-    return 2
+    return 127
   else
     local PRG="$1"; shift
     "$SCALA_HOME/bin/$PRG" "$@"