docs: Fix a couple typos.

This commit is contained in:
Mateusz Mandera
2019-03-02 01:50:32 +01:00
committed by Tim Abbott
parent b4f35bd54e
commit 6a540d5773
2 changed files with 2 additions and 2 deletions

View File

@@ -145,7 +145,7 @@ materials](https://developers.google.com/open-source/gsoc/resources/manual).
for even complex changes. for even complex changes.
- Or Eklavya Sharma's (from GSoC 2016) to see a fellow GSoC student doing - Or Eklavya Sharma's (from GSoC 2016) to see a fellow GSoC student doing
this well. (`git log -p` `--``author=Eklavya` is a fast way to skim). this well. (`git log -p --author=Eklavya` is a fast way to skim).
- Team up with other developers close to or in your time zone who are working - Team up with other developers close to or in your time zone who are working
on similar areas to trade timely initial code reviews. 75% of the feedback on similar areas to trade timely initial code reviews. 75% of the feedback

View File

@@ -121,7 +121,7 @@ HEAD is now at 5a1e982 tools: Update clean-branches to clean review branches.
are merging other users' commits into a Zulip repository. After doing are merging other users' commits into a Zulip repository. After doing
`reset-to-pull-request` or `fetch-pull-request` and making some `reset-to-pull-request` or `fetch-pull-request` and making some
changes, you can push a branch back to a pull request with e.g. changes, you can push a branch back to a pull request with e.g.
`tools/push-to-pull-rqeuest 1234`. This is useful for a few things: `tools/push-to-pull-request 1234`. This is useful for a few things:
* Getting CI to run and enabling you to use the GitHub "Merge" buttons * Getting CI to run and enabling you to use the GitHub "Merge" buttons
to merge a PR after you make some corrections to a PR, without to merge a PR after you make some corrections to a PR, without