doc: fix "edit source" widget (#1597) #16

	#
	# Build HTML documentation and upload it to GitHub Pages
	#

	name: Build and deploy documentation

	on:
	push:
	paths:
	- 'documentation/*/.rst'
	- 'documentation/**/conf.py'

	# This enables the Run Workflow button on the Actions tab.
	workflow_dispatch:

	jobs:
	build-documentation:
	runs-on: ${{ matrix.os }}
	strategy:
	matrix:
	os: [ubuntu-latest]

	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive

	#
	# Build documentation installing first 'furo' theme dependencies
	#

	- uses: ammaraskar/sphinx-action@master
	with:
	pre-build-command: "echo furo >> documentation/requirements.txt"
	docs-folder: "documentation"

	- name: Deploy documents to GH pages
	uses: JamesIves/github-pages-deploy-action@v4
	with:
	folder: documentation/_build/html

Provide feedback