Admin/init_components
author haftmann
Tue, 26 Jun 2012 22:25:36 +0200
changeset 48152 f06697f776b0
parent 48151 a80595d4f850
child 48154 2709937c7430
permissions -rw-r--r--
support for platform-specific components

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

for COMPONENTS_FILE in "${ISABELLE_HOME}/Admin/components" "${ISABELLE_HOME}/Admin/components.${ML_PLATFORM}"
do
  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 < "${COMPONENTS_FILE}"
done