Deploy docs via git push
this MR implements the option to deploy the docs via git-push
to a dedicated branch. it is implemented as an alternative option for the deploy_pages_in_ci
parameter and will push the docs to the gh-pages
branch (that is used by GitHub Pages).