changeset 33286 | 1807921b6268 |
parent 32390 | 468eff174a77 |
child 33294 | e2a11715aab1 |
--- a/lib/scripts/getsettings Wed Oct 28 18:21:02 2009 +0100 +++ b/lib/scripts/getsettings Wed Oct 28 20:49:09 2009 +0100 @@ -86,7 +86,7 @@ local COMPONENT="$1" if [ ! -d "$COMPONENT" ]; then - echo >&2 "Bad Isabelle component: $COMPONENT" + echo >&2 "Bad Isabelle component: \"$COMPONENT"\" exit 2 elif [ -z "$ISABELLE_COMPONENTS" ]; then ISABELLE_COMPONENTS="$COMPONENT"