1 files changed, 42 insertions, 11 deletions

diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index e4359f70..9864fd4d 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -1,11 +1,34 @@
 #!/usr/bin/env bash
 
-# Usage: dev/tools/backport-pr.sh <PR number> [--stop-before-merging]
-
 set -e
 
-PRNUM=$1
-OPTION=$2
+if [[ $# == 0 ]]; then
+    echo "Usage: $0 [--no-conflict] [--no-signature-check] [--stop-before-merging] prnum"
+    exit 1
+fi
+
+while [[ $# -gt 0 ]]; do
+    case "$1" in
+        --no-conflict)
+            NO_CONFLICTS="true"
+            shift
+            ;;
+        --no-signature-check)
+            NO_SIGNATURE_CHECK="true"
+            shift
+            ;;
+        --stop-before-merging)
+            STOP_BEFORE_MERGING="true"
+            shift
+            ;;
+        *)
+            if [[ "$PRNUM" != "" ]]; then
+                echo "PRNUM was already set to $PRNUM and is now being overridden with $1."
+            fi
+            PRNUM="$1"
+            shift
+    esac
+done
 
 if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then
     echo "PR #${PRNUM} does not exist."
@@ -14,7 +37,7 @@ fi
 
 SIGNATURE_STATUS=$(git log master --grep "Merge PR #${PRNUM}" --format="%G?")
 git log master --grep "Merge PR #${PRNUM}" --format="%GG"
-if [[ "${SIGNATURE_STATUS}" != "G" ]]; then
+if [[ "$NO_SIGNATURE_CHECK" != "true" && "$SIGNATURE_STATUS" != "G" ]]; then
     echo
     read -p "Merge commit does not have a good (valid) signature. Bypass? [y/N] " -n 1 -r
     echo
@@ -27,9 +50,17 @@ BRANCH=backport-pr-${PRNUM}
 RANGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%P" | sed 's/ /../')
 MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merge/Backport/')
 
-if git checkout -b ${BRANCH}; then
+if git checkout -b "${BRANCH}"; then
 
-    if ! git cherry-pick -x ${RANGE}; then
+    if ! git cherry-pick -x "${RANGE}"; then
+        if [[ "$NO_CONFLICTS" == "true" ]]; then
+            git status
+            echo "Conflicts! Aborting..."
+            git cherry-pick --abort
+            git checkout -
+            git branch -d "$BRANCH"
+            exit 1
+        fi
         echo "Please fix the conflicts, then exit."
         bash
         while ! git cherry-pick --continue; do
@@ -50,7 +81,7 @@ else
 
 fi
 
-if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then
+if ! git diff --exit-code HEAD "${BRANCH}" -- "*.mli"; then
     echo
     read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r
     echo
@@ -59,12 +90,12 @@ if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then
     fi
 fi
 
-if [[ "${OPTION}" == "--stop-before-merging" ]]; then
+if [[ "$STOP_BEFORE_MERGING" == "true" ]]; then
     exit 0
 fi
 
-git merge -S --no-ff ${BRANCH} -m "${MESSAGE}"
-git branch -d ${BRANCH}
+git merge -S --no-ff "${BRANCH}" -m "${MESSAGE}"
+git branch -d "${BRANCH}"
 
 # To-Do:
 # - Support for backporting a PR before it is merged