# -*- 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"