diff options
author | Pietro Albini <pietro@pietroalbini.org> | 2019-10-17 15:09:40 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-17 15:09:40 +0200 |
commit | 86a17d6d956b976dcd628b079189b554abef5d9d (patch) | |
tree | 7a3bfb69d62441c2b3357f9f0000d6deb47b9798 | |
parent | 9b84e0b8ba156e706a1ed58c4a8def012e11bbc5 (diff) | |
parent | 3ee40cf89416a0d633ba8ba7cc672cdc3a2ccb75 (diff) |
Merge pull request #152 from Manishearth/dt-github
Fixup devtools team github perms
-rw-r--r-- | config.toml | 1 | ||||
-rw-r--r-- | teams/devtools.toml | 3 |
2 files changed, 4 insertions, 0 deletions
diff --git a/config.toml b/config.toml index 5159efb..9260d60 100644 --- a/config.toml +++ b/config.toml @@ -7,4 +7,5 @@ allowed-mailing-lists-domains = [ allowed-github-orgs = [ "rust-lang", "rust-lang-nursery", + "rust-dev-tools", ] diff --git a/teams/devtools.toml b/teams/devtools.toml index 6a6dc97..072d56e 100644 --- a/teams/devtools.toml +++ b/teams/devtools.toml @@ -18,6 +18,9 @@ repo = "https://github.com/rust-dev-tools/dev-tools-team" discord-invite = "https://discord.gg/sG23nSS" discord-name = "#dev-tools" +[github] +orgs = ["rust-lang", "rust-dev-tools"] + [[lists]] address = "tools@rust-lang.org" |