Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-06-16 13:34:26 -0700 (Fri, 16 Jun 2006)
Revision: 9336
Log message:

      The "jyh: this option needs to be documented in Chapter~\ref{chapter:rules}"
      is no longer relevant.