equal
deleted
inserted
replaced
29 ISABELLE_IDENTIFIER="" |
29 ISABELLE_IDENTIFIER="" |
30 |
30 |
31 #users tend to put strange things in here ... |
31 #users tend to put strange things in here ... |
32 unset ENV |
32 unset ENV |
33 unset BASH_ENV |
33 unset BASH_ENV |
|
34 unset POSIXLY_CORRECT |
|
35 set +o posix |
34 |
36 |
35 #support easy settings |
37 #support easy settings |
36 function choosefrom () |
38 function choosefrom () |
37 { |
39 { |
38 local RESULT="" |
40 local RESULT="" |
103 \#* | "") ;; |
105 \#* | "") ;; |
104 /*) init_component "$REPLY" ;; |
106 /*) init_component "$REPLY" ;; |
105 *) init_component "$COMPONENT/$REPLY" ;; |
107 *) init_component "$COMPONENT/$REPLY" ;; |
106 esac |
108 esac |
107 done |
109 done |
108 } < "$COMPONENT/etc/components" |
110 } < <( cat "$COMPONENT/etc/components"; echo; ) |
109 fi |
111 fi |
110 } |
112 } |
111 |
113 |
112 #main components |
114 #main components |
113 init_component "$ISABELLE_HOME" |
115 init_component "$ISABELLE_HOME" |