Releasing

This will bump the version, create a tag and push it to GitHub. GH Actions takes care of releasing to PyPi and updating the documentation.

git checkout master
git pull origin master
make version-minor (or `make version-major` / `make version-patch`)
git push --follow-tags

Finally, manually create a release on GitHub

• Create release
• Select the right tag
• Press "generate release notes" (top right above the release description edit box)
• Publish release