PR #388 Acknowledge removal of a clippy lint

Acknowledge removal of a clippy lint #388

HadrienG2 merged 1 commit into main from removed-clippy-lint

Remove removed clippy lint

305fc3ac

HadrienG2 enabled auto-merge 8 days ago

HadrienG2 merged c6740703 into main 8 days ago

HadrienG2 deleted the removed-clippy-lint branch 8 days ago

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Milestone

No milestone