diff options
| author | bors <bors@rust-lang.org> | 2024-10-09 12:21:58 +0000 |
|---|---|---|
| committer | bors <bors@rust-lang.org> | 2024-10-09 12:21:58 +0000 |
| commit | 87058a499093b2d919849c6edeb643c5ba03a438 (patch) | |
| tree | 9ded9362198af916f7dc9f3d32c973e7779bcdc5 | |
| parent | edc5c1ec1ce4f9f3b6abcd6764d57b6068ad43dc (diff) | |
| parent | f90c97c915f69369e167d4d0eeff8ac914ebb764 (diff) | |
| download | rust-87058a499093b2d919849c6edeb643c5ba03a438.tar.gz rust-87058a499093b2d919849c6edeb643c5ba03a438.zip | |
Auto merge of #3955 - RalfJung:review-bot, r=RalfJung
CONTRIBUTING.md: explain the review bot use
| -rw-r--r-- | src/tools/miri/CONTRIBUTING.md | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/tools/miri/CONTRIBUTING.md b/src/tools/miri/CONTRIBUTING.md index 7a32962886c..d0bcf68eacb 100644 --- a/src/tools/miri/CONTRIBUTING.md +++ b/src/tools/miri/CONTRIBUTING.md @@ -45,6 +45,14 @@ process for such contributions: This process is largely informal, and its primary goal is to more clearly communicate expectations. Please get in touch with us if you have any questions! +### Managing the review state + +Most PRs bounce back and forth between the reviewer and the author several times, so it is good to +keep track of who is expected to take the next step. We are using the `S-waiting-for-review` and +`S-waiting-for-author` labels for that. If a reviewer asked you to do some changes and you think +they are all taken care of, post a comment saying `@rustbot ready` to mark a PR as ready for the +next round of review. + ## Preparing the build environment Miri heavily relies on internal and unstable rustc interfaces to execute MIR, |