tree bc1e603f265d2d8a6dc783d4d73de6cf88b7f63c
parent eb662aa07a1e2394169ca26fa6f1376a076c7d55
author Mike Pennisi <mike@mikepennisi.com> 1560802733 -0400
committer Robert Ma <bob1211@gmail.com> 1560815278 -0400

[docs] Build (but do not deploy) for pull requests

Although the documentation website should not be rebuilt in response to
pull requests, refusing to simply build the site may potentially hide
errors during the review process.

Update the documentation generation script to build the site as part of
the pull request, provided a relevant file has been modified. With this
applied, if the patch under review regresses the script, the contributor
and reviewers are immediately notified.