diff options
| author | Pierre Courtieu | 2018-04-11 11:08:23 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2018-04-11 15:03:34 +0200 |
| commit | d1d67a41cad8723815403533dee161c0e4a42c59 (patch) | |
| tree | 94b526f0e32a7d133c6ad2c881ad8deba1b6d4d7 /dev/doc | |
| parent | 8059a0efa79fcd72d56c424adf1bea10dae28d6d (diff) | |
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 3a2df6a81f..84ff94c66a 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 |