ci: publish documentation on merge When a commit is pushed or merged into one of the release branches (master, maint/*) then push the documentation update to gh-pages.
2019-02-17T19:07:37