Skip to content

Conversation

@einarf
Copy link
Member

@einarf einarf commented Jan 19, 2023

Cherry pick PR from maintenance + typo fixes + conflict resolve

Just saw this contradiction on the website and thought I could quickly fix it.
@einarf einarf merged commit 8dd0e59 into development Jan 19, 2023
@einarf einarf deleted the maint-cherry-pick branch January 22, 2023 19:06
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