Skip to content

get rid of tidy 'unnecessarily ignored' warnings#98717

Merged
bors merged 1 commit intorust-lang:masterfrom RalfJung:make-tidy-less-annoyingJul 1, 2022
+4-9

Commits

Commits on Jun 30, 2022