| author | blanchet |
| Thu, 26 Jul 2012 11:08:16 +0200 | |
| changeset 49549 | 2307efbfc554 |
| parent 49463 | 94c11abc5a52 |
| child 49857 | ac976e51cb67 |
| 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 |
|
| wenzelm@49463 | 8 |
while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
|
| haftmann@49165 | 9 |
do |
| wenzelm@49463 | 10 |
case "$REPLY" in |
| haftmann@49181 | 11 |
\#* | "") ;; |
| wenzelm@49463 | 12 |
/*) init_component "$REPLY" ;; |
| wenzelm@49463 | 13 |
*) init_component "$COMPONENT/$REPLY" ;; |
| haftmann@49181 | 14 |
esac |
| wenzelm@49463 | 15 |
done < "$ISABELLE_HOME/Admin/components" |