lib/scripts/getsettings
changeset 40570 bf8f92bdf630
parent 40568 3003be923908
child 41511 2fe62d602681
equal deleted inserted replaced
40569:ffcff7509a49 40570:bf8f92bdf630
    89 #nested components
    89 #nested components
    90 ISABELLE_COMPONENTS=""
    90 ISABELLE_COMPONENTS=""
    91 function init_component ()
    91 function init_component ()
    92 {
    92 {
    93   local COMPONENT="$1"
    93   local COMPONENT="$1"
       
    94   case "$COMPONENT" in
       
    95     /*) ;;
       
    96     *)
       
    97       echo >&2 "Absolute component path required: \"$COMPONENT\""
       
    98       exit 2
       
    99       ;;
       
   100   esac
    94 
   101 
    95   if [ ! -d "$COMPONENT" ]; then
   102   if [ ! -d "$COMPONENT" ]; then
    96     echo >&2 "Bad Isabelle component: \"$COMPONENT\""
   103     echo >&2 "Bad Isabelle component: \"$COMPONENT\""
    97     exit 2
   104     exit 2
    98   elif [ -z "$ISABELLE_COMPONENTS" ]; then
   105   elif [ -z "$ISABELLE_COMPONENTS" ]; then