lib/scripts/getsettings
changeset 41760 bf49b7a85936
parent 41759 6aa5804aaf90
child 43519 024bd7f5ee0f
equal deleted inserted replaced
41759:6aa5804aaf90 41760:bf49b7a85936
   132     ISABELLE_COMPONENTS="$COMPONENT"
   132     ISABELLE_COMPONENTS="$COMPONENT"
   133   else
   133   else
   134     ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   134     ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   135   fi
   135   fi
   136   if [ -f "$COMPONENT/etc/settings" ]; then
   136   if [ -f "$COMPONENT/etc/settings" ]; then
   137     source "$COMPONENT/etc/settings" || exit 2
   137     source "$COMPONENT/etc/settings"
       
   138     local RC="$?"
       
   139     if [ "$RC" -ne 0 ]; then
       
   140       echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
       
   141       exit 2
       
   142     fi
   138   fi
   143   fi
   139   if [ -f "$COMPONENT/etc/components" ]; then
   144   if [ -f "$COMPONENT/etc/components" ]; then
   140     {
   145     {
   141       while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   146       while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   142       do
   147       do