lib/scripts/getsettings
changeset 41760 bf49b7a85936
parent 41759 6aa5804aaf90
child 43519 024bd7f5ee0f
--- 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
     {