Fix more warnings
In particular, the ones found by core/dune-grid!542
Edited by Oliver Sander
In particular, the ones found by core/dune-grid!542
marked this merge request as draft
marked this merge request as ready
mentioned in commit be82d2cc
merged