aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-08 12:45:45 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-08 12:45:45 +0100
commit02f96d47c46a36995444aa46e7dc48c6016fc614 (patch)
treec828c5f3965e2363f3577e861e4c22b65848f2e5 /dev
parentc3426f7a449349aca875c922c3ed448e4a750b41 (diff)
parent8eacdda782791bf4a7b58bdf19e4ca1bbd01a705 (diff)
Merge PR #6527: Update backport script for more control.
Diffstat (limited to 'dev')
-rwxr-xr-xdev/tools/backport-pr.sh7
1 files changed, 6 insertions, 1 deletions
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index 4c4dbe1e9..d7acf01f1 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}