Remove the legacy version of symbol_search(). #270


	name: Deploy documentation

	on:
	# Every push onto the main branch regerenates the documentation
	push:
	branches:
	- 'master'

	jobs:

	do-deploy:
	runs-on: ubuntu-latest
	name: 'Build documentation on Linux'
	steps:

	- uses: actions/checkout@v2

	- name: Install dependencies
	run: \|
	sudo apt update -qq
	sudo apt install -y make autoconf python3-sphinx

	- name: Make Documentation
	run: \|
	cd Documentation
	make html

	- name: Deploy to GitHub Pages
	uses: crazy-max/ghaction-github-pages@v2
	with:
	target_branch: gh-pages
	build_dir: Documentation/_build/html
	jekyll: false
	env:
	GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

Provide feedback