equal
deleted
inserted
replaced
84 function init_component () |
84 function init_component () |
85 { |
85 { |
86 local COMPONENT="$1" |
86 local COMPONENT="$1" |
87 |
87 |
88 if [ ! -d "$COMPONENT" ]; then |
88 if [ ! -d "$COMPONENT" ]; then |
89 echo >&2 "Bad Isabelle component: $COMPONENT" |
89 echo >&2 "Bad Isabelle component: \"$COMPONENT"\" |
90 exit 2 |
90 exit 2 |
91 elif [ -z "$ISABELLE_COMPONENTS" ]; then |
91 elif [ -z "$ISABELLE_COMPONENTS" ]; then |
92 ISABELLE_COMPONENTS="$COMPONENT" |
92 ISABELLE_COMPONENTS="$COMPONENT" |
93 else |
93 else |
94 ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" |
94 ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" |