Skip to content

Merge main into develop#64

Merged
barthanssens merged 6 commits intodevelopfrom
main
Aug 30, 2025
Merged

Merge main into develop#64
barthanssens merged 6 commits intodevelopfrom
main

Conversation

@github-actions
Copy link

@github-actions github-actions bot commented Apr 1, 2025

Automatically generated PR to keep develop in sync with main.

USE MERGE COMMIT TO MERGE THIS PR.

See merge_main_to_develop.yml.

hmottestad and others added 6 commits March 15, 2025 16:03
* javadocs for 5.1.1

Signed-off-by: Håvard Ottestad <hmottestad@gmail.com>

* news item and release-notes if relevant for 5.1.1

Signed-off-by: Håvard Ottestad <hmottestad@gmail.com>

* wip

* update Acknowledgements

---------

Signed-off-by: Håvard Ottestad <hmottestad@gmail.com>
@barthanssens barthanssens merged commit 175cebd into develop Aug 30, 2025
4 of 5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants