From 6d1e99e96e632c193430fe073958700d451bb703 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sun, 27 Nov 2022 20:47:49 +0100 Subject: [PATCH] advice on josh pushing --- src/tools/miri/CONTRIBUTING.md | 7 +++++++ 1 file changed, 7 insertions(+) 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: