diff options
Diffstat (limited to 'src/tools')
| -rwxr-xr-x | src/tools/publish_toolstate.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tools/publish_toolstate.py b/src/tools/publish_toolstate.py index 24d6fd5b19b..3688812fe0a 100755 --- a/src/tools/publish_toolstate.py +++ b/src/tools/publish_toolstate.py @@ -15,7 +15,7 @@ except ImportError: # List of people to ping when the status of a tool changed. MAINTAINERS = { 'miri': '@oli-obk @RalfJung @eddyb', - 'clippy-driver': '@Manishearth @llogiq @mcarton @oli-obk', + 'clippy-driver': '@Manishearth @llogiq @mcarton @oli-obk @phansch', 'rls': '@nrc @Xanewok', 'rustfmt': '@nrc @topecongiro', 'book': '@carols10cents @steveklabnik', |