less brutal return from function, to allow caller to report error;
authorwenzelm
Sun, 01 Apr 2012 22:02:14 +0200
changeset 47254 de2fb19683f4
parent 47253 a00c5c88d8f3
child 47257 fd85c8a29827
less brutal return from function, to allow caller to report error;
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" "$@"
 }