upgrade.
Description:
Release used to copy the updated release_docs/HISTORY.txt and
release_docs/RELEASE.txt to the doc/html/ADGuide. The doc/ is
removed from the source tree. So, remove the command that
does the copying.
Note that once the separated doc/ location is known, release needs
to copy the two files into them and committed them via sub-version
commands.
Platforms tested:
No test because it is a trivial change and it is not easy to change
without triggering the full release process.
Misc. update:
cd5ca85fb7