> > Is this an oversight, or are these options deprecated? > > These options are intentionally not documented: they should not be > used by programmers. Perhaps we should add a comment to common.opt to explain this? Ben