Added part-install to centaur/bitops.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2961 303c5b2c-9740-0410-b014-fd8f9db7be32
Added a script to move/copy ACL2 builds, that creates run_acl2,
a wrapper to saved_acl2, which when run for the first time
additionally fixes the relocated cert files avoiding costly
recertification.

Usage:
./make-dist.sh <ACL2 build path name>  <new path name>

Then in the new path 
./run_acl2



git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2962 303c5b2c-9740-0410-b014-fd8f9db7be32
Made documentation updates to reflect acl2-devel changes:

- Added the following to :doc note-7-0:

  The utility :[pl2] no longer automatically instantiates free
  variables; similarly for calls of :[pl] on a term. Thanks to Eric
  Smith for sending an example showing the problem with the previous
  implementation.

  We removed support for legacy [documentation] topics
  SWITCHES-PARAMETERS-AND-MODES and the ``Tours''. (The
  implementation-level change was to remove such entries from source
  function documentation-alist-stub.) While the community-books and
  ACL2-only documentation continues to be maintained, existing
  old-style (pre-[xdoc]) documentation topics that use those deleted
  topics as a parent will likely need to have a different parent.

- Added the following comment to (defxdoc note-7-0 ...) in
  community book books/system/doc/acl2-doc.lisp:

; We now avoid a raw Lisp error for encapsulate events occurring when trying to
; check for redundancy.  The problem was that getprop was being called by
; find-first-non-local-name with a non-symbol first argument.  Thanks to Jared
; Davis for reporting this bug by sending the following example:
;
;   (encapsulate () ((x)))

- Updated :doc with-output, mostly to explain the following change
  just made in acl2-devel to remove the :trace keyword:

  The :trace keyword has been removed from with-evisc-tuple and the
  :evisc argument to with-output, because the evisc-tuple for tracing
  has an unusual under-the-hood implementation that makes it difficult
  to support that keyword.


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2963 303c5b2c-9740-0410-b014-fd8f9db7be32
ccg/README: added :dir :system to the include-book forms

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2964 303c5b2c-9740-0410-b014-fd8f9db7be32
fix-cert-fn now identifies situations where the acl2-systems-book directories are themselves different and accordingly gives them as the old-dir and new-dir. The earlier behavior used the complete dir name of a book, instead of the systems-book-dir. Both behaviors are supported, the earlier heavior is kept because it checks the simple tests in this directory.

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