acl2/acl2 — pull request #293 by ragerdl (2014-10-23 16:19:16+00:00)
Title: Improve std::define and add reference to xdoc when users are looking for 

@jaredcdavis Please review this change to std::define and perform this merge request.

Kaufmann patches std::define such that it now provides a :redundant output when a define is redundant.
Fixes #220

Adding a reference to the xdoc topic from 'books-certification' and 'build-the-manual'. Also changed the canonical command used to build the manual. I considered listing both commands but decided less to read was better.
Fixes #289.