From 9bf16fa5c450a5a3e377e6415ab33bb3c4f80077 Mon Sep 17 00:00:00 2001
From: Jourdan Luca <luca.jourdan@etu.univ-lyon1.fr>
Date: Thu, 12 Jul 2018 15:22:25 +0200
Subject: [PATCH] issue #4681

Signed-off-by: Andrea Maria Piana <andrea.maria.piana@gmail.com>
---
 scripts/merge-pr.sh | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/scripts/merge-pr.sh b/scripts/merge-pr.sh
index d69b83a043..b80795a9c3 100755
--- a/scripts/merge-pr.sh
+++ b/scripts/merge-pr.sh
@@ -37,6 +37,22 @@ check_pr_prereq() {
   fi
 }
 
+check_sync() {
+    git fetch
+    if [ -n "$(git rev-list $BRANCH..$REMOTE/$BRANCH)" ]; then
+      warn "the local branch $BRANCH is behind $REMOTE/$BRANCH."
+      echo "Do you want to cancel or do you prefer to abandon your work and reset local $BRANCH to $REMOTE/$BRANCH ?"
+      echo "cancel/reset"
+      read response;
+      if [ "$response" = "reset" ]; then
+          git fetch $REMOTE
+          git reset --hard $REMOTE/$BRANCH
+      else
+          fatal "the local branch $BRANCH is behind $REMOTE/$BRANCH."
+      fi
+    fi
+}
+
 GH_URL_BASE="https://api.github.com"
 
 get_pr_info() {
@@ -133,6 +149,7 @@ EOF
   fi
   load_config
   check_pr_prereq
+  check_sync
   get_pr_info "$@"
   cleanup
   fetch_pr