Commit 2a4e866a43e3db1e2be8e2a3d986ddc9f855d2bc
2019-02-17T12:34:23
ci: publish documentation after merge When a continuous integration build runs (ie a commit is pushed or merged into one of the CI branches, `master` or `maint/*`) then push the rebuilt documentation into the `gh-pages` branch.