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