#29: change target branch for docs deployment #1

	name: Deploy docs

	on:
	push:
	branches: [ develop, 29-deploy-docs-on-pushes-to-develop ]

	jobs:
	build-and-deploy-docs:
	runs-on: ubuntu-latest
	env:
	docs-directory: /home/runner/work/pressio/pressio-ops/docs
	python-version: '3.10'

	steps:
	- uses: actions/checkout@v3
	- name: Set up Python ${{ env.python-version }}
	uses: actions/setup-python@v4
	with:
	python-version: ${{ env.python-version }}
	architecture: 'x64'
	- name: Install Python dependencies
	run: \|
	pip3 install -r ./docs/build_requirements.txt
	- name: Build documentation
	working-directory: ${{ env.docs-directory }}
	run: \|
	make html
	# .nojekyll file is needed for GitHub Pages to know it's getting a ready webpage
	# and there is no need to generate anything
	- name: Generate nojekyll file
	working-directory: ${{ env.docs-directory }}/generated_docs
	run: touch .nojekyll
	# This action moves the content of `generated_docs` to the branch from where
	# the site is published
	- name: Deploy docs
	uses: JamesIves/github-pages-deploy-action@v4
	with:
	branch: website-deployment
	folder: ${{ env.docs-directory }}/generated_docs
	clean: true

Provide feedback