On 01/10/15 06:05, Richard Sandiford wrote:
Thanks. I didn't realize there was a disagreement when I approved. Let's continue to hash this out a bit in the hopes that we can all get to a place where we're comfortable with the final change, whatever it happens to me.Sorry for the slow response. Jeff has approved the patch in the meantime, but I didn't want to go ahead and apply it while there was still disagreement...
jeff