Build and deploy documentation site to GitHub Pages based on repo contents #807

	name: Build and deploy documentation site to GitHub Pages based on repo contents

	# This runner generated documentation using a python script
	# For the methodology on publishing the documentation on the same github pages account as the main site, see this: https://deanattali.com/blog/multiple-github-pages-domains/

	on:
	push:
	# branches:
	# - release

	workflow_dispatch:

	jobs:
	build:
	# Add "id-token" with the intended permissions.
	permissions:
	contents: 'read'
	id-token: 'write'

	runs-on: ubuntu-latest

	steps:
	- name: checkout repo content
	uses: actions/checkout@v4 # checkout the repository content to github runner.

	- name: setup python
	uses: actions/setup-python@v5
	with:
	python-version: 3.11 #install the python needed

	- run: pip install markdown glob2 urllib3 beautifulsoup4 Pygments md_ext mkdocs_custom_fences

	- name: execute py script # run the run.py to get the latest data
	run: \|
	python mk_docs.py 2>&1

	- name: Deploy
	uses: peaceiris/actions-gh-pages@v4
	with:
	personal_token: ${{ secrets.PAT_TOKEN }}
	publish_dir: ./_site

Provide feedback