| changeset 49006 | 0febe9e433dd |
| parent 49005 | 96d5e42e5e3a |
| child 49007 | f781bbe0d91b |
| 49005:96d5e42e5e3a | 49006:0febe9e433dd |
|---|---|
1 # -*- shell-script -*- :mode=shellscript: |
|
2 # |
|
3 # Author: Florian Haftmann, TU Muenchen |
|
4 # |
|
5 # init_components - bash source script to initialize components |
|
6 # as specified in the Admin directory |
|
7 |
|
8 while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } |
|
9 do |
|
10 case "$REPLY" in |
|
11 \#* | "") ;; |
|
12 /*) init_component "$REPLY" ;; |
|
13 *) init_component "$COMPONENT/$REPLY" ;; |
|
14 esac |
|
15 done < "$ISABELLE_HOME/Admin/components_old" |