changeset 48448 | 94c11abc5a52 |
parent 47996 | 25b9f59ab1b9 |
child 48455 | a509f19d4cc6 |
--- a/lib/scripts/getsettings Mon Jul 23 15:59:14 2012 +0200 +++ b/lib/scripts/getsettings Mon Jul 23 16:13:26 2012 +0200 @@ -163,8 +163,7 @@ esac if [ ! -d "$COMPONENT" ]; then - echo >&2 "Missing Isabelle component directory: \"$COMPONENT\"" - exit 2 + echo >&2 "### Missing Isabelle component: \"$COMPONENT\"" elif [ -z "$ISABELLE_COMPONENTS" ]; then ISABELLE_COMPONENTS="$COMPONENT" else