From 8eacdda782791bf4a7b58bdf19e4ca1bbd01a705 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 24 Dec 2017 13:42:12 +0100
Subject: Update backport script for more control.

---
 dev/tools/backport-pr.sh | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'dev/tools')

diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index 4c4dbe1e97..d7acf01f1d 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -1,10 +1,11 @@
 #!/usr/bin/env bash
 
-# Usage: dev/tools/backport-pr.sh <PR number>
+# Usage: dev/tools/backport-pr.sh <PR number> [--stop-before-merging]
 
 set -e
 
 PRNUM=$1
+OPTION=$2
 
 if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then
     echo "PR #${PRNUM} does not exist."
@@ -49,6 +50,10 @@ else
 
 fi
 
+if [[ "${OPTION}" == "--stop-before-merging" ]]; then
+    exit 0
+fi
+
 git merge -S --no-ff ${BRANCH} -m "${MESSAGE}"
 git branch -d ${BRANCH}
 
-- 
cgit v1.2.3