clarified init_component: always liberal;
authorwenzelm
Mon Jul 23 16:13:26 2012 +0200 (2012-07-23)
changeset 4844894c11abc5a52
parent 48447 ef600ce4559c
child 48449 2d987dad7c3e
clarified init_component: always liberal;
reduced divergence of clone from lib/scripts/getsettings;
Admin/init_components
lib/scripts/getsettings
     1.1 --- a/Admin/init_components	Mon Jul 23 15:59:14 2012 +0200
     1.2 +++ b/Admin/init_components	Mon Jul 23 16:13:26 2012 +0200
     1.3 @@ -5,22 +5,11 @@
     1.4  # init_components - bash source script to initialize components
     1.5  # as specified in the Admin directory
     1.6  
     1.7 -function init_component_liberal
     1.8 -{
     1.9 -  local LOCATION="$1"
    1.10 -  if [[ -d "${LOCATION}" ]]
    1.11 -  then
    1.12 -    init_component "${LOCATION}"
    1.13 -  else
    1.14 -    echo "Warning: no component found in ${LOCATION}" >&2
    1.15 -  fi
    1.16 -}
    1.17 -
    1.18 -while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
    1.19 +while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
    1.20  do
    1.21 -  case "${REPLY}" in
    1.22 +  case "$REPLY" in
    1.23      \#* | "") ;;
    1.24 -    /*) init_component_liberal "${REPLY}" ;;
    1.25 -    *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
    1.26 +    /*) init_component "$REPLY" ;;
    1.27 +    *) init_component "$COMPONENT/$REPLY" ;;
    1.28    esac
    1.29 -done < "${ISABELLE_HOME}/Admin/components"
    1.30 +done < "$ISABELLE_HOME/Admin/components"
     2.1 --- a/lib/scripts/getsettings	Mon Jul 23 15:59:14 2012 +0200
     2.2 +++ b/lib/scripts/getsettings	Mon Jul 23 16:13:26 2012 +0200
     2.3 @@ -163,8 +163,7 @@
     2.4    esac
     2.5  
     2.6    if [ ! -d "$COMPONENT" ]; then
     2.7 -    echo >&2 "Missing Isabelle component directory: \"$COMPONENT\""
     2.8 -    exit 2
     2.9 +    echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
    2.10    elif [ -z "$ISABELLE_COMPONENTS" ]; then
    2.11      ISABELLE_COMPONENTS="$COMPONENT"
    2.12    else