Quoting :doc note-6-5-books:

  Certification of books under models/y86 has a much cleaner
  implementation in GNUmakefile, with the result that are no longer
  certified by the make target, all. For ACL2(h) and host Lisps that
  can handle this task, they are certified by the target, everything,
  and there the user's -j option to make is no longer ignored.

Executed the following command in each of oslib/tests/, xdoc/tests/,
and centaur/vl/loader/lexer/:

  svn propset -R svn:ignore -F /projects/acl2/devel/books/unversioned-files.txt .

Documented ACL2 improvements in :doc note-6-5:

  The [brr@] command now supports inputs :initial-ttree and
  :final-ttree. Thanks to David Rager for a request leading to these
  enhancements. See [ttree] for a discussion of the tag-tree
  structures returned for these inputs.

  (GCL only) A restriction for structure-sharing (as described in a
  remark, ``Remark on print-circle-files''; see [print-control])
  involving GCL has been removed, since this is no longer required
  for the latest GCL versions (2.6.8 and 2.6.10). Thanks to Jared
  Davis and Camm Maguire for useful discussions and this GCL
  improvement.


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2499 303c5b2c-9740-0410-b014-fd8f9db7be32