/* FIXME: should change weighting variable, etc. */
/* These control the ordering produced by
compare_variables_given_ordering(). */
/* FIXME: should change weighting variable, etc. */
/* These control the ordering produced by
compare_variables_given_ordering(). */