diff options
author | Pietro Albini <pietro@pietroalbini.org> | 2019-02-20 17:15:37 +0100 |
---|---|---|
committer | Pietro Albini <pietro@pietroalbini.org> | 2019-02-20 17:15:37 +0100 |
commit | fe2019f73fa8ab4ecb6ac3d2af2b17373663310c (patch) | |
tree | 02952d276115c308ccf76766c40ae0f60d2adbe0 /README.md | |
parent | 91423bc3131ef275bbd63a00f1a93235c69cf71e (diff) |
document the crater permission
Diffstat (limited to 'README.md')
-rw-r--r-- | README.md | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -133,4 +133,6 @@ permissions are available: [permissions] # Optional, grants access to the @rust-timer GitHub bot perf = true +# Optional, grants access to the @craterbot GitHub bot +crater = true ``` |