summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--people/RalfJung.toml1
-rw-r--r--src/permissions.rs1
-rw-r--r--teams/compiler.toml1
3 files changed, 3 insertions, 0 deletions
diff --git a/people/RalfJung.toml b/people/RalfJung.toml
index ef8ab0e..bc26e2e 100644
--- a/people/RalfJung.toml
+++ b/people/RalfJung.toml
@@ -4,3 +4,4 @@ github = "RalfJung"
[permissions]
perf = true
bors.rust.review = true
+bors.miri.review = true
diff --git a/src/permissions.rs b/src/permissions.rs
index bd947b2..5901cb8 100644
--- a/src/permissions.rs
+++ b/src/permissions.rs
@@ -139,6 +139,7 @@ permissions! {
crater,
crates_io,
hashbrown,
+ miri,
libc,
regex,
rls,
diff --git a/teams/compiler.toml b/teams/compiler.toml
index 2311243..91e32ef 100644
--- a/teams/compiler.toml
+++ b/teams/compiler.toml
@@ -20,6 +20,7 @@ members = [
perf = true
crater = true
bors.rust.review = true
+bors.miri.review = true
[rfcbot]
label = "T-compiler"