| author | blanchet |
| Mon, 23 Jul 2012 15:32:30 +0200 | |
| changeset 49448 | 9e9b6e363859 |
| 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"
|