Skip to content

Commit 1a9ba3b

Browse files
committed
Add note, that a merge commit after push is necessary
1 parent 842dd07 commit 1a9ba3b

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

CONTRIBUTING.md

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -178,6 +178,15 @@ to be run inside the `rust` directory):
178178
_Note:_ This will directly push to the remote repository. You can also push
179179
to your local copy by replacing the remote address with `/path/to/rust-clippy`
180180
directory.
181+
182+
_Note:_ Most of the time you have to create a merge commit in the
183+
`rust-clippy` repo (this has to be done in the Clippy repo, not in the
184+
rust-copy of Clippy):
185+
```bash
186+
git checkout sync-from-rust
187+
git fetch upstream
188+
git merge upstream/master
189+
```
181190
3. Open a PR to `rust-lang/rust-clippy` and wait for it to get merged (to
182191
accelerate the process ping the `@rust-lang/clippy` team in your PR and/or
183192
~~annoy~~ ask them in the [Discord] channel.)

0 commit comments

Comments
 (0)