Updated :doc books-certification to reflect the new meaning of "make all" for book regressions. Fixed a bit of obsolete wording in ./GNUmakefile.

I don't claim to have caught all places where the documentation needs
updating to reflect the recent changes in books/GNUmakefile, but I
happened to notice one in :doc books-certification, which I've fixed
as mentioned above.

I hope that others will keep an eye out for additional such
documentation updates that need to be made due to yesterday's
books/GNUmakefile changes.

Thanks to Eric Smith for pointing out the obsolete wording in
a comment in ./GNUmakefile.

Author: MattKaufmann

GNUmakefile

@@ -36,8 +36,7 @@
 #   make TAGS        ; Create tags table, handy for viewing sources with emacs.
 #   make TAGS!       ; Same as TAGS, except forces a rebuild of TAGS.
 #   make regression
-#                    ; Certify most community books and, if present, the
-#                    ; workshops/ books as well.
+#                    ; Certify most community books.
 #   make regression ACL2=xxx
 #                    ; Same as make regression, but use xxx as ACL2, which
 #                    ; should either be an absolute filename or a command on

books/system/doc/acl2-doc.lisp

@@ -10219,9 +10219,9 @@ That said, it is easy to do: just run @('make all'), e.g.,</p>
     $ make ACL2=/path/to/acl2-sources/saved_acl2 -j 2 all
 })
 
-<p>This actually still skips a few books that are very slow.  If you
-<i>really</i> need to certify absolutely everything, you can run @('make
-everything'), but this will likely add hours to your build!</p>
+<p>This includes a few books that are quite slow to certify.  You can
+exclude those by replacing ``@('all')'' by ``@('regression')'' in the
+command above.</p>
 
 
 <h3>Cleaning Up</h3>

doc.lisp

@@ -12887,9 +12887,9 @@ A Full Build
     $ cd /path/to/acl2-sources/books
     $ make ACL2=/path/to/acl2-sources/saved_acl2 -j 2 all
 
-  This actually still skips a few books that are very slow.  If you
-  really need to certify absolutely everything, you can run make
-  everything, but this will likely add hours to your build!
+  This includes a few books that are quite slow to certify.  You can
+  exclude those by replacing ``all'' by ``regression'' in the command
+  above.
 
 
 Cleaning Up

doc/acl2-code-size.txt

@@ -10,5 +10,5 @@ Source files (not including doc.lisp):
   258529 lines,  11309867 characters
 ------------------------------------
 Documentation (file books/system/doc/acl2-doc.lisp):
-  131136 lines,   5794327 characters
+  131136 lines,   5794280 characters
 ------------------------------------

doc/home-page.html

@@ -152,7 +152,7 @@
 <center>
 <b><a href="mailto:kaufmann@cs.utexas.edu">Matt Kaufmann</a> and <a href="mailto:moore@cs.utexas.edu">J Strother Moore</a></b><br>
 <a href="http://www.utexas.edu">University of Texas at Austin</a><br>
-July 30, 2020
+July 31, 2020
 </center>
 
 <p>