On Friday, February 28, 2003, at 03:03 PM, Richard Henderson wrote: > I'll bootstrap your patch, change the name of the option, and > apply it as-is, i.e. disabled by default. We can address the > other issues raised as a followup. Thank you.