those changes break miri, PR will be issued later
This commit is contained in:
parent
043d873b32
commit
9d52cb2f84
@ -23,7 +23,7 @@
|
|||||||
# Each tool has a list of people to ping
|
# Each tool has a list of people to ping
|
||||||
|
|
||||||
# ping @oli-obk @RalfJung @eddyb
|
# ping @oli-obk @RalfJung @eddyb
|
||||||
miri = "Testing"
|
miri = "Broken"
|
||||||
|
|
||||||
# ping @Manishearth @llogiq @mcarton @oli-obk
|
# ping @Manishearth @llogiq @mcarton @oli-obk
|
||||||
clippy = "Broken"
|
clippy = "Broken"
|
||||||
|
Loading…
Reference in New Issue
Block a user