* _build/Dockerfile.build: New Dockerfile for docs-build pipeline,
with the required tools for building the docs installed.
* _build/Jenkinsfile.build: New Jenkinsfile defining the docs-build
pipeline.

Change-Id: If50e687a5b9342eb2dcb5cb39e8a63db91f8616d