Making a release

1. In github, go to releases
2. Draft a new release
3. Create a tag using a YY.MM.DDmicro, for example 24.11.26a
4. Click Generate release notes
5. Publish release