# HG changeset patch
# User wenzelm
# Date 1333310534 -7200
# Node ID de2fb19683f405c712fd363c5df8432d59fcb68a
# Parent  a00c5c88d8f3e1fe3a342be46b54bc148c0fe4e7
less brutal return from function, to allow caller to report error;

diff -r a00c5c88d8f3 -r de2fb19683f4 lib/scripts/getsettings
--- 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" "$@"
 }