diff options
Diffstat (limited to 'src/tools/publish_toolstate.py')
| -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 04a1d257bc0..fe5195738c1 100755 --- a/src/tools/publish_toolstate.py +++ b/src/tools/publish_toolstate.py @@ -30,7 +30,7 @@ except ImportError: # These should be collaborators of the rust-lang/rust repository (with at least # read privileges on it). CI will fail otherwise. MAINTAINERS = { - 'miri': {'oli-obk', 'RalfJung', 'eddyb'}, + 'miri': {'oli-obk', 'RalfJung'}, 'rls': {'Xanewok'}, 'rustfmt': {'topecongiro', 'calebcartwright'}, 'book': {'carols10cents', 'steveklabnik'}, |