From d1d67a41cad8723815403533dee161c0e4a42c59 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 11 Apr 2018 11:08:23 +0200
Subject: merge script support https + typos in doc

---
 dev/doc/MERGING.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/doc')

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
-- 
cgit v1.2.3