less brutal return from function, to allow caller to report error;
authorwenzelm
Sun Apr 01 22:02:14 2012 +0200 (2012-04-01)
changeset 47254de2fb19683f4
parent 47253 a00c5c88d8f3
child 47257 fd85c8a29827
less brutal return from function, to allow caller to report error;
lib/scripts/getsettings
     1.1 --- a/lib/scripts/getsettings	Sun Apr 01 21:46:45 2012 +0200
     1.2 +++ b/lib/scripts/getsettings	Sun Apr 01 22:02:14 2012 +0200
     1.3 @@ -92,7 +92,7 @@
     1.4  #robust invocation via ISABELLE_JDK_HOME
     1.5  function isabelle_jdk () {
     1.6    [ -z "$ISABELLE_JDK_HOME" ] && \
     1.7 -    { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable"; exit 2; }
     1.8 +    { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2; return 2; }
     1.9    local PRG="$1"; shift
    1.10    "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
    1.11  }
    1.12 @@ -100,7 +100,7 @@
    1.13  #robust invocation via SCALA_HOME
    1.14  function isabelle_scala () {
    1.15    [ -z "$SCALA_HOME" ] && \
    1.16 -    { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; }
    1.17 +    { echo "Unknown SCALA_HOME -- Scala unavailable" >&2; return 2; }
    1.18    local PRG="$1"; shift
    1.19    "$SCALA_HOME/bin/$PRG" "$@"
    1.20  }