diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/MERGING.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 3a2df6a81..84ff94c66 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -70,7 +70,7 @@ To merge the PR proceed in the following way ``` $ git checkout master $ git pull -$ dev/tools/merge-pr XXXX +$ dev/tools/merge-pr.sh XXXX $ git push upstream ``` where `XXXX` is the number of the PR to be merged and `upstream` is the name |