+Array<String>
+split_string (String s, char c)
+{
+ Array<String> rv;
+ while (s.length ())
+ {
+ int i = s.index (c);
+
+ if (i == 0)
+ {
+ s = s.nomid_string (0, 1);
+ continue;
+ }
+
+ if (i < 0)
+ i = s.length ();
+
+ rv.push (s.cut_string (0, i));
+ s = s.nomid_string (0, i);
+ }
+
+ return rv;
+}