Closed Philipp91 closed 2 years ago
Fixes #137
No idea if this reintroduces a lint error that 812ca1779f9537153d57fd89a08c6957361d93ac tried to solve -- we'll see.
Fixes #137
No idea if this reintroduces a lint error that 812ca1779f9537153d57fd89a08c6957361d93ac tried to solve -- we'll see.