--- a/lib/scripts/getsettings Sun Apr 01 21:46:45 2012 +0200
+++ b/lib/scripts/getsettings Sun Apr 01 22:02:14 2012 +0200
@@ -92,7 +92,7 @@
#robust invocation via ISABELLE_JDK_HOME
function isabelle_jdk () {
[ -z "$ISABELLE_JDK_HOME" ] && \
- { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable"; exit 2; }
+ { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2; return 2; }
local PRG="$1"; shift
"$ISABELLE_JDK_HOME/bin/$PRG" "$@"
}
@@ -100,7 +100,7 @@
#robust invocation via SCALA_HOME
function isabelle_scala () {
[ -z "$SCALA_HOME" ] && \
- { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; }
+ { echo "Unknown SCALA_HOME -- Scala unavailable" >&2; return 2; }
local PRG="$1"; shift
"$SCALA_HOME/bin/$PRG" "$@"
}