changeset 32390 | 468eff174a77 |
parent 32321 | 13920dbe4547 |
child 33286 | 1807921b6268 |
--- a/lib/scripts/getsettings Fri Aug 21 19:06:12 2009 +0200 +++ b/lib/scripts/getsettings Sat Aug 22 17:08:06 2009 +0200 @@ -68,6 +68,17 @@ done } +#arrays +function splitarray () +{ + SPLITARRAY=() + local IFS="$1"; shift + for X in $* + do + SPLITARRAY["${#SPLITARRAY[@]}"]="$X" + done +} + #nested components ISABELLE_COMPONENTS="" function init_component ()