Automatically create GitHub releases

[nitishr]

Closes #749.

Introduces a new GitHub Actions workflow that automates the creation of GitHub releases. The workflow is triggered on push events to tags that start with 'v', and it extracts release notes from the RELEASE.md file based on the tag version. The extracted notes are then used as the body of the created release.

Future considerations:

• Streamline more/the rest of the release process and reduce manual effort.
• Do this in a CircleCI instead of a GitHub workflow for uniformity and lower cognitive load. I didn't do that here because I didn't have the github token for use in CircleCI.

Testing

Verified the outcome of this workflow by updating RELEASE.md and pushing a tag to a local branch. The created release contains the extracted notes for just that release.

[floehopper]

@nitishr This looks good to me - thank you!

Streamline more/the rest of the release process and reduce manual effort.

Agreed.

Do this in a CircleCI instead of a GitHub workflow for uniformity and lower cognitive load. I didn't do that here because I didn't have the github token for use in CircleCI.

I think I'd probably move the CI build to GitHub Actions instead unless you can think of a good reason not to.

Verified the outcome of this workflow by updating RELEASE.md and pushing a tag to a local branch. The created release contains the extracted notes for just that release.

Thanks for testing it. I'd quite like to retrospectively create releases for all the existing release tags, so perhaps I can use the same (or a similar) script to do that when I have time and use that as a bit of a test...?