diff -r 6aa5804aaf90 -r bf49b7a85936 lib/scripts/getsettings --- a/lib/scripts/getsettings Sun Feb 13 17:29:44 2011 +0100 +++ b/lib/scripts/getsettings Sun Feb 13 17:45:21 2011 +0100 @@ -134,7 +134,12 @@ ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" fi if [ -f "$COMPONENT/etc/settings" ]; then - source "$COMPONENT/etc/settings" || exit 2 + source "$COMPONENT/etc/settings" + local RC="$?" + if [ "$RC" -ne 0 ]; then + echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\"" + exit 2 + fi fi if [ -f "$COMPONENT/etc/components" ]; then {