Commit 5a443ade9f65d6a5dc9bcd977e0f38dedd36207e

Khaled Hosny 2025-07-29T22:30:33

[ci] Add a script to extract release notes from NEWS file Add a script to extract the release notes from the NEWS files and use them when creating GitHub releases, so that we don’t need to copy them manually. Add also a test to make sure the NEWS file always have release notes for the current release.