init_component: require absolute path (when invoked by user scripts);
authorwenzelm
Tue Nov 16 21:54:52 2010 +0100 (2010-11-16)
changeset 40570bf8f92bdf630
parent 40569 ffcff7509a49
child 40571 fbac01813bff
init_component: require absolute path (when invoked by user scripts);
lib/scripts/getsettings
     1.1 --- a/lib/scripts/getsettings	Tue Nov 16 21:48:14 2010 +0100
     1.2 +++ b/lib/scripts/getsettings	Tue Nov 16 21:54:52 2010 +0100
     1.3 @@ -91,6 +91,13 @@
     1.4  function init_component ()
     1.5  {
     1.6    local COMPONENT="$1"
     1.7 +  case "$COMPONENT" in
     1.8 +    /*) ;;
     1.9 +    *)
    1.10 +      echo >&2 "Absolute component path required: \"$COMPONENT\""
    1.11 +      exit 2
    1.12 +      ;;
    1.13 +  esac
    1.14  
    1.15    if [ ! -d "$COMPONENT" ]; then
    1.16      echo >&2 "Bad Isabelle component: \"$COMPONENT\""