update clippy

RalfJung · RalfJung · commit 09307474c28e · 2019-08-11T12:06:12.000+02:00
diff --git a/src/tools/clippy b/src/tools/clippy
@@ -1 +1 @@
-Subproject commit b041511b5fcd386c4ae74a30b60a5081f8717fbe
+Subproject commit 72da1015d6d918fe1b29170acbf486d30e0c2695
