doc: Move github pages to the documentation repo (#566) #77

	name: Update GH Pages
	on:
	workflow_dispatch:
	push:
	branches:
	- main
	paths:
	- docs_src/**
	# pull_request:
	# The branches below must be a subset of the branches above
	# branches: [ "main" ]
	jobs:
	deploy:
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v2
	- uses: actions/setup-python@v2
	with:
	python-version: 3.x
	- name: Install mkdocs
	run: \|
	pip install mkdocs
	pip install mkdocs-material
	pip install mkdocs-swagger-ui-tag
	pip install mike
	- name: Configure Git user
	run: \|
	git config --local user.email "github-actions[bot]@users.noreply.github.com"
	git config --local user.name "github-actions[bot]"
	- name: Deploy
	run: mike deploy latest

Provide feedback