Skip to content

Fix a clippy warning#198

Merged
poljar merged 1 commit into
mainfrom
poljar/clippy-fix
Jul 22, 2026
Merged

Fix a clippy warning#198
poljar merged 1 commit into
mainfrom
poljar/clippy-fix

Conversation

@poljar

@poljar poljar commented Jul 22, 2026

Copy link
Copy Markdown
Collaborator

No description provided.

@poljar
poljar requested a review from richvdh July 22, 2026 09:02

@richvdh richvdh left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

oops. Thanks. Wonder why CI didn't spot this.

@poljar

poljar commented Jul 22, 2026

Copy link
Copy Markdown
Collaborator Author

oops. Thanks. Wonder why CI didn't spot this.

Your PR, #195, depended on main before #190 was merged. #190 was merged before your PR was merged but after it passed CI.

@poljar
poljar merged commit 8414857 into main Jul 22, 2026
7 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.

2 participants