Script for Jenkins documentation build

Script for Jenkins documentation build

Move the script to do the documentation build from Jenkins to the
repository to reduce coupling.  There is hardly any content in the
script that would need to change if something in Jenkins changes (and
those few details can easily be passed into the script), but a lot that
needs to be changed whenever the build system for the documentation is
refined.

For now, the contents are essentially the same as in the Jenkins job
configuration for Documentation_Gerrit_master or
Documentation_Nightly_master.  Having a script in the same repository as
the build system makes it easier to evolve the script and the build
system in sync without enforcing rebases for every change in Gerrit.

Change-Id: If5eda21c94bc7d4707d4716d4f54b2be3ae898cf