# -*- shell-script -*- :mode=shellscript:

 #

 # Author: Florian Haftmann, TU Muenchen

 #

 # init_components - bash source script to initialize components

 # as specified in the Admin directory

 function init_component_liberal

 {

   local LOCATION="$1"

   if [[ -d "${LOCATION}" ]]

   then

     init_component "${LOCATION}"

   else

     echo "Warning: no component found in ${LOCATION}" >&2

   fi

 }

 while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }

 do

   case "${REPLY}" in

     \#* | "") ;;

     /*) init_component_liberal "${REPLY}" ;;

     *) init_component_liberal "${COMPONENT}/${REPLY}" ;;

   esac

 done < "${ISABELLE_HOME}/Admin/components"