+# Script arguments are handled uniformly as follows:
+# - If the argument does not contain a '|' character, it is appended
+# to both command lines.
+# - If the argument has a '|' character in it, the text on either side
+# of the '|' is appended to the respective command lines. Note that
+# you'll have to quote the arg or escape the '|' with a backslash
+# so that the shell doesn't think you're doing a pipe.
+# - Arguments with '#' characters are split at those characters,
+# processed for alternatives ('|'s) as independent terms, then
+# pasted back into a single argument (without the '#'s). (Sort of
+# inspired by the C preprocessor '##' token pasting operator.)
+#
+# In other words, the arguments should look like the command line you
+# want to run, with "|" used to list the alternatives for the parts
+# that you want to differ between the two runs.
+#
+# For example:
+#
+# % tracediff m5.opt --opt1 '--opt2|--opt3' --opt4
+# would compare these two runs:
+# m5.opt --opt1 --opt2 --opt4
+# m5.opt --opt1 --opt3 --opt4
+#
+# % tracediff 'path1|path2#/m5.opt' --opt1 --opt2
+# would compare these two runs:
+# path1/m5.opt --opt1 --opt2
+# path2/m5.opt --opt1 --opt2