Skip to content
This repository was archived by the owner on Nov 25, 2025. It is now read-only.

Fix CI#102

Merged
yoshuawuyts merged 1 commit intomainfrom
fix-ci
Sep 16, 2025
Merged

Fix CI#102
yoshuawuyts merged 1 commit intomainfrom
fix-ci

Conversation

@yoshuawuyts
Copy link
Copy Markdown
Member

Fixes the CI failure introduced in #96. Thanks.

@yoshuawuyts
Copy link
Copy Markdown
Member Author

Self-merging this since it's not a material change to the actual proposal, and we need CI to pass to do the releases.

@yoshuawuyts yoshuawuyts merged commit 6442be9 into main Sep 16, 2025
1 check passed
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant