Philipp Hansch 5114050839
Update lint deprecation for tool lints
Our lint deprecation previously didn't work for tool lints, because
`register_removed` was registering lints to be removed _without_ the
`clippy` prefix.
2019-08-12 19:20:36 +02:00
..
2019-08-12 19:20:36 +02:00
2019-06-21 16:47:34 +02:00
2019-07-28 06:45:23 +02:00
2019-06-21 16:47:34 +02:00