+# Split command line arguments which can be separated by either commas
+# or whitespace. If dwim is set, it will complain about string ending
+# in comma since this usually means someone did 'madison -a i386, m68k
+# foo' or something and the inevitable confusion resulting from 'm68k'
+# being treated as an argument is undesirable.
+
+def split_args (s, dwim=1):
+ if s.find(",") == -1:
+ return s.split();
+ else:
+ if s[-1:] == "," and dwim:
+ fubar("split_args: found trailing comma, spurious space maybe?");
+ return s.split(",");
+
+################################################################################
+