equal
deleted
inserted
replaced
66 CLASSPATH="$CLASSPATH:$X" |
66 CLASSPATH="$CLASSPATH:$X" |
67 fi |
67 fi |
68 done |
68 done |
69 } |
69 } |
70 |
70 |
|
71 #arrays |
|
72 function splitarray () |
|
73 { |
|
74 SPLITARRAY=() |
|
75 local IFS="$1"; shift |
|
76 for X in $* |
|
77 do |
|
78 SPLITARRAY["${#SPLITARRAY[@]}"]="$X" |
|
79 done |
|
80 } |
|
81 |
71 #nested components |
82 #nested components |
72 ISABELLE_COMPONENTS="" |
83 ISABELLE_COMPONENTS="" |
73 function init_component () |
84 function init_component () |
74 { |
85 { |
75 local COMPONENT="$1" |
86 local COMPONENT="$1" |