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, 13 Feb 2011 17:45:21 +0100
changeset 41760 bf49b7a85936
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
--- 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
     {