Add workflow_dispatch #225

	# This action is triggered whenever push to the docs folder of the master branch is made.
	# It generates HTML pages from the docs folder of the master branch and push them to the gh-pages branch.

	name: Build user documentation pages
	on:
	push:
	branches: 'master'
	paths: 'docs/**'
	workflow_dispatch
Check failure on line 9 in .github/workflows/docs_builder.yml View workflow run for this annotation GitHub Actions / .github/workflows/docs_builder.yml Invalid workflow file `You have an error in your yaml syntax on line 9`

	jobs:
	build:
	runs-on: ubuntu-latest
	steps:
	- name: Install Sphinx
	run: pip install -U Sphinx==7.3.7

	- name: Install Theme
	run: pip install sphinx-rtd-theme

	- name: Checkout master
	uses: actions/checkout@master
	with:
	path: 'master'

	- name: Checkout gh-pages
	uses: actions/checkout@master
	with:
	path: 'gh_pages'
	ref: 'gh-pages'

	- name: Build user documentation
	run: sphinx-build -b html "${GITHUB_WORKSPACE}/master/docs" "${GITHUB_WORKSPACE}/gh_pages/docs"

	- name: Push changes in gh-pages
	run: \|
	cd "${GITHUB_WORKSPACE}/gh_pages"
	date > generated.txt
	git config user.name github-actions
	git config user.email github-actions@github.com
	git add .
	git commit -m "update user documentation bot"
	git push

Provide feedback