diff options
| author | Oli Scherer <git-spam-no-reply9815368754983@oli-obk.de> | 2022-06-27 16:08:19 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-06-27 16:08:19 +0200 |
| commit | dfb592a91d69d1df6d131deaf5b72d0341a0f9cc (patch) | |
| tree | 44f6386bae4b27a2687232fbbf03350cfd4dc503 /src/tools/publish_toolstate.py | |
| parent | bd2e51a338e36372b200a22f3e0e22189a1063e6 (diff) | |
| download | rust-dfb592a91d69d1df6d131deaf5b72d0341a0f9cc.tar.gz rust-dfb592a91d69d1df6d131deaf5b72d0341a0f9cc.zip | |
Remove eddyb from miri failure pings
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'}, |