lib/scripts/getsettings
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 ()