On Thu, 17 Jul 2003, Ben Elliston wrote: >> Sigh. I thought that we were discussing fixing the manual, not >> renaming options. > It's kind of important that they're both fixed ;-) As there seems to be agreement, would you mind adding this to the table in codingconventions.html? (Trivially pre-approved.) Thanks, Gerald