diff options
| author | Pietro Albini <pietro@pietroalbini.org> | 2019-09-03 13:06:48 +0200 |
|---|---|---|
| committer | Pietro Albini <pietro@pietroalbini.org> | 2019-09-03 20:21:19 +0200 |
| commit | 5f51210cc08b466d5ebc53448c8b150c82b0ef80 (patch) | |
| tree | 7fde58f97eaf6a4a4c9581871410644f83774a82 | |
| parent | 02c4da1699dcdcdb2aefa4f51c9640312bbf1d52 (diff) | |
bump clippy
| m--------- | src/tools/clippy | 33 |
1 files changed, 21 insertions, 12 deletions
diff --git a/src/tools/clippy b/src/tools/clippy -Subproject 72da1015d6d918fe1b29170acbf486d30e0c269 +Subproject 3aea86030eeca7dff94139b24d6b76294609dbc |