David Lechner eeca2c3cbe github: Add GitHub action to build docs. ...

This builds docs, but only on pull requests that change a file in the
docs/ directory.

2020-06-05 21:42:10 +10:00

..

workflows

github: Add GitHub action to build docs.

2020-06-05 21:42:10 +10:00