author | bulwahn |
Sat, 21 Jul 2012 10:53:26 +0200 | |
changeset 49429 | 43875bab3a4c |
parent 49181 | 1bee47c0c278 |
child 49463 | 94c11abc5a52 |
permissions | -rw-r--r-- |
haftmann@49165 | 1 |
# -*- shell-script -*- :mode=shellscript: |
haftmann@49165 | 2 |
# |
haftmann@49165 | 3 |
# Author: Florian Haftmann, TU Muenchen |
haftmann@49165 | 4 |
# |
haftmann@49165 | 5 |
# init_components - bash source script to initialize components |
haftmann@49165 | 6 |
# as specified in the Admin directory |
haftmann@49165 | 7 |
|
haftmann@49165 | 8 |
function init_component_liberal |
haftmann@49165 | 9 |
{ |
haftmann@49165 | 10 |
local LOCATION="$1" |
haftmann@49166 | 11 |
if [[ -d "${LOCATION}" ]] |
haftmann@49166 | 12 |
then |
haftmann@49166 | 13 |
init_component "${LOCATION}" |
haftmann@49166 | 14 |
else |
haftmann@49169 | 15 |
echo "Warning: no component found in ${LOCATION}" >&2 |
haftmann@49166 | 16 |
fi |
haftmann@49165 | 17 |
} |
haftmann@49165 | 18 |
|
haftmann@49181 | 19 |
while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; } |
haftmann@49165 | 20 |
do |
haftmann@49181 | 21 |
case "${REPLY}" in |
haftmann@49181 | 22 |
\#* | "") ;; |
haftmann@49181 | 23 |
/*) init_component_liberal "${REPLY}" ;; |
haftmann@49181 | 24 |
*) init_component_liberal "${COMPONENT}/${REPLY}" ;; |
haftmann@49181 | 25 |
esac |
haftmann@49181 | 26 |
done < "${ISABELLE_HOME}/Admin/components" |