1
Fork 0

Remove miri from the submodule list and require it for CI to pass

This commit is contained in:
Oli Scherer 2022-09-19 19:08:02 +00:00
parent d9382d03bd
commit 6cfa7ef2ba
12 changed files with 136 additions and 217 deletions

View file

@ -356,7 +356,7 @@ cc = ["@ehuss"]
cc = ["@rust-lang/clippy"]
[mentions."src/tools/miri"]
message = "The Miri submodule was changed"
message = "The Miri subtree was changed"
cc = ["@rust-lang/miri"]
[mentions."src/tools/rustfmt"]