Admin/init_components
author haftmann
Tue, 26 Jun 2012 22:09:34 +0200
changeset 48150 c97656ff4154
child 48151 a80595d4f850
permissions -rw-r--r--
snippet to be sourced in user settings file in order to initialize components for a repository revision; the initialization is Ā»liberalĀ« since there is no obvious solution yet for components whose distribution is restricted

# -*- 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"
  [[ -d "${LOCATION}" ]] || echo "Warning: no component found in ${LOCATION}" && return
  init_component "${LOCATION}"
}

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"