diff options
| author | Ralf Jung <post@ralfj.de> | 2022-11-27 20:47:49 +0100 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2022-11-27 20:52:17 +0100 |
| commit | 6d1e99e96e632c193430fe073958700d451bb703 (patch) | |
| tree | a3a572d4f5f29cd88320e3e205a1be4feeb50b71 /src | |
| parent | 7c12ed1d5dc6059972b06fb7257a239f3a33ec88 (diff) | |
| download | rust-6d1e99e96e632c193430fe073958700d451bb703.tar.gz rust-6d1e99e96e632c193430fe073958700d451bb703.zip | |
advice on josh pushing
Diffstat (limited to 'src')
| -rw-r--r-- | src/tools/miri/CONTRIBUTING.md | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/tools/miri/CONTRIBUTING.md b/src/tools/miri/CONTRIBUTING.md index 5f46e2af0f9..c63f356607d 100644 --- a/src/tools/miri/CONTRIBUTING.md +++ b/src/tools/miri/CONTRIBUTING.md @@ -296,6 +296,13 @@ needed. ### Exporting changes to the rustc repo +Keep in mind that pushing is the most complicated job that josh has to do -- +pulling just filters the rustc history, but pushing needs to construct a new +rustc history that would filter to the given Miri history! To avoid problems, it +is a good idea to always pull immediately before you push. In particular, you +should never do two josh pushes without an intermediate pull; that can lead to +duplicated commits. + Josh needs to be running, as described above. We will use the josh proxy to push to your fork of rustc. Run the following in the Miri repo, assuming we are on an up-to-date master branch: |