Admin/init_components
changeset 48150 c97656ff4154
child 48151 a80595d4f850
equal deleted inserted replaced
48149:9cb0abdf7c07 48150:c97656ff4154
       
     1 # -*- shell-script -*- :mode=shellscript:
       
     2 #
       
     3 # Author: Florian Haftmann, TU Muenchen
       
     4 #
       
     5 # init_components - bash source script to initialize components
       
     6 # as specified in the Admin directory
       
     7 
       
     8 function init_component_liberal
       
     9 {
       
    10   local LOCATION="$1"
       
    11   [[ -d "${LOCATION}" ]] || echo "Warning: no component found in ${LOCATION}" && return
       
    12   init_component "${LOCATION}"
       
    13 }
       
    14 
       
    15 while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
       
    16 do
       
    17   case "${REPLY}" in
       
    18     \#* | "") ;;
       
    19     /*) init_component_liberal "${REPLY}" ;;
       
    20     *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
       
    21   esac
       
    22 done < "${ISABELLE_HOME}/Admin/components"