Merge pull request #2060 from fchapoton/fix_some_typos #307

	# Workflow to push documentation to website
	#
	# To work on the wheel building infrastructure on a fork, comment out:
	#
	# if: github.repository == 'flintlib/flint'

	name: Deploy

	on:
	push:
	branches:
	- main
	paths:
	- 'doc/**'
	- '.github/workflows/docs.yml'

	jobs:
	##############################################################################
	# build documentation
	##############################################################################
	build-doc:
	name: Push documentation to website
	if: github.repository == 'flintlib/flint'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	with:
	fetch-depth: 2

	- name: "Setup"
	run: \|
	sudo apt-get install -y python3-sphinx
	sphinx-build --version

	- name: "Build documentation"
	run: \|
	cd doc
	make html SPHINXOPTS="-W -j auto"

	- name: "Build pdf documentation"
	uses: dante-ev/latex-action@latest
	with:
	root_file:
	compiler:
	args:
	entrypoint: doc/entrypoint.sh

	- name: "Create a tarball of the documentation"
	run: \|
	cd doc/build
	mv html doc
	cp latex/Flint.pdf doc
	tar -czvf doc.tar.gz doc

	- name: "Setup SSH key"
	uses: shimataro/[email protected]
	with:
	key: ${{ secrets.SSH_KEY }}
	name: id_ed25519
	known_hosts: ${{ secrets.KNOWN_HOSTS }}

	- name: "Push documentation to server"
	run: \|
	cd doc/build
	ssh -t [email protected] 'mkdir ~/tmp'
	scp doc.tar.gz [email protected]:~/tmp
	ssh -t [email protected] 'cd ~/tmp && tar -xf doc.tar.gz && rm -rf ~/apps/flintlib_org/doc && mv doc ~/apps/flintlib_org && cd ~ && rm -rf ~/tmp'

Provide feedback