diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-19 13:35:29 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-19 13:35:29 +0200 |
| commit | 9a4ca53a3a021cb16de7706ec79a26e49f54de49 (patch) | |
| tree | b1d6a2f65920cdc7e00b5705855bab83ac484113 /dev/doc | |
| parent | d799b6a6117258583919dc4e518afd92b23a05ed (diff) | |
| parent | d1d67a41cad8723815403533dee161c0e4a42c59 (diff) | |
Merge PR #7219: merge script support https + typos in doc
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 |