author | wenzelm |
Wed, 28 Oct 2009 20:49:09 +0100 | |
changeset 33286 | 1807921b6268 |
parent 33285 | a0de1d5c7b3d |
child 33287 | 0f99569d23e1 |
--- 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"