more explicit exit due to failed etc/settings -- normally return code 0=true and 1=false could be tolerated, but bash syntax errors also return 1;
authorwenzelm
Sun Feb 13 17:45:21 2011 +0100 (2011-02-13)
changeset 41760bf49b7a85936
parent 41759 6aa5804aaf90
child 41761 2dc75bae5226
more explicit exit due to failed etc/settings -- normally return code 0=true and 1=false could be tolerated, but bash syntax errors also return 1;
lib/scripts/getsettings
     1.1 --- a/lib/scripts/getsettings	Sun Feb 13 17:29:44 2011 +0100
     1.2 +++ b/lib/scripts/getsettings	Sun Feb 13 17:45:21 2011 +0100
     1.3 @@ -134,7 +134,12 @@
     1.4      ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
     1.5    fi
     1.6    if [ -f "$COMPONENT/etc/settings" ]; then
     1.7 -    source "$COMPONENT/etc/settings" || exit 2
     1.8 +    source "$COMPONENT/etc/settings"
     1.9 +    local RC="$?"
    1.10 +    if [ "$RC" -ne 0 ]; then
    1.11 +      echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
    1.12 +      exit 2
    1.13 +    fi
    1.14    fi
    1.15    if [ -f "$COMPONENT/etc/components" ]; then
    1.16      {