Quoting :doc note-6-5:

  The utility [sys-call+] can now only be called if there is an active
  [trust-tag], which is the restriction that was already in place for
  [sys-call]. This plugs a potential soundness hole.

  The default value for the :write-port keyword argument of
  [certify-book] is now t, as was already claimed by the
  documentation. Thus, a .port file will be written when a book is
  certified, making it more likely that a subsequent [include-book]
  will complete without error even if the book has been modified
  without recertification. Note that a change by Sol Swords to the
  build system for the [community-books] now sets an environment
  variable to guarantee that write-port is true, independent of this
  change.  On a related note: the unadvertised environment
  variable ACL2_WRITE_PORT is now handled more appropriately, by
  interning its upcased argument into the ACL2 package.

Also updated a bit of documentation relevant to sys-call and sys-call+.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1262 5d84a466-a78b-0930-a311-59b22171a541