Add note, that a merge commit after push is necessary

This commit is contained in:
flip1995 2020-05-19 16:36:14 +02:00
parent 842dd07261
commit 1a9ba3b2c2
No known key found for this signature in database
GPG key ID: 2CEFCDB27ED0BE79

View file

@ -178,6 +178,15 @@ to be run inside the `rust` directory):
_Note:_ This will directly push to the remote repository. You can also push
to your local copy by replacing the remote address with `/path/to/rust-clippy`
directory.
_Note:_ Most of the time you have to create a merge commit in the
`rust-clippy` repo (this has to be done in the Clippy repo, not in the
rust-copy of Clippy):
```bash
git checkout sync-from-rust
git fetch upstream
git merge upstream/master
```
3. Open a PR to `rust-lang/rust-clippy` and wait for it to get merged (to
accelerate the process ping the `@rust-lang/clippy` team in your PR and/or
~~annoy~~ ask them in the [Discord] channel.)