# 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" "$@" }