Admin/init_components
changeset 48448 94c11abc5a52
parent 48166 1bee47c0c278
child 48842 ac976e51cb67
equal deleted inserted replaced
48447:ef600ce4559c 48448:94c11abc5a52
     3 # Author: Florian Haftmann, TU Muenchen
     3 # Author: Florian Haftmann, TU Muenchen
     4 #
     4 #
     5 # init_components - bash source script to initialize components
     5 # init_components - bash source script to initialize components
     6 # as specified in the Admin directory
     6 # as specified in the Admin directory
     7 
     7 
     8 function init_component_liberal
     8 while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
     9 {
       
    10   local LOCATION="$1"
       
    11   if [[ -d "${LOCATION}" ]]
       
    12   then
       
    13     init_component "${LOCATION}"
       
    14   else
       
    15     echo "Warning: no component found in ${LOCATION}" >&2
       
    16   fi
       
    17 }
       
    18 
       
    19 while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
       
    20 do
     9 do
    21   case "${REPLY}" in
    10   case "$REPLY" in
    22     \#* | "") ;;
    11     \#* | "") ;;
    23     /*) init_component_liberal "${REPLY}" ;;
    12     /*) init_component "$REPLY" ;;
    24     *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
    13     *) init_component "$COMPONENT/$REPLY" ;;
    25   esac
    14   esac
    26 done < "${ISABELLE_HOME}/Admin/components"
    15 done < "$ISABELLE_HOME/Admin/components"