Fix clippy errors
Fixed clippy errors not caught before merging !204 (merged). Maybe we should enforce a Clippy check for all types of merge requests.
Edited by Benjamin Gallois
Fixed clippy errors not caught before merging !204 (merged). Maybe we should enforce a Clippy check for all types of merge requests.