equal
deleted
inserted
replaced
161 exit 2 |
161 exit 2 |
162 ;; |
162 ;; |
163 esac |
163 esac |
164 |
164 |
165 if [ ! -d "$COMPONENT" ]; then |
165 if [ ! -d "$COMPONENT" ]; then |
166 echo >&2 "Missing Isabelle component directory: \"$COMPONENT\"" |
166 echo >&2 "### Missing Isabelle component: \"$COMPONENT\"" |
167 exit 2 |
|
168 elif [ -z "$ISABELLE_COMPONENTS" ]; then |
167 elif [ -z "$ISABELLE_COMPONENTS" ]; then |
169 ISABELLE_COMPONENTS="$COMPONENT" |
168 ISABELLE_COMPONENTS="$COMPONENT" |
170 else |
169 else |
171 ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" |
170 ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" |
172 fi |
171 fi |