diff --git a/docs/source/developers/github/pull_request.rst b/docs/source/developers/github/pull_request.rst index 2eef0ffe6..cdc49aaed 100644 --- a/docs/source/developers/github/pull_request.rst +++ b/docs/source/developers/github/pull_request.rst @@ -33,7 +33,7 @@ After submitting a pull request, you may get comments from reviewer that somethi #. Push the new commit to remote repository. Then the commit will be displayed in pull request automatically. :: - $git push origin + $git push origin -f Resolving Conflit in the Pull Request ------------------------------------ @@ -63,7 +63,7 @@ During the reviewing of your pull request, some one may change certain code whic #. Push the change to the remote repository :: - $git push origin + $git push origin -f Then you will see the pull request is enabled to be merged automatically.