From fe3977512f18c269e82765995ee1e9ba5d6e4b43 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Date: Sun, 8 Apr 2018 20:34:06 +0200
Subject: Add sanity check in merge script: local branch is up-to-date.

In case the local branch is ahead of upstream, we only print
a warning because it could be that we are merging several
PRs in a row.
---
 dev/tools/merge-pr.sh | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'dev/tools')

diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index c4ee2aa73..60e3d739c 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -110,6 +110,26 @@ if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then
   ask_confirmation
 fi;
 
+# Sanity check: the local branch is up-to-date with upstream
+
+LOCAL_BRANCH_COMMIT=$(git rev-parse HEAD)
+UPSTREAM_COMMIT=$(git rev-parse @{u})
+if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then
+
+    # Is it just that the upstream branch is behind?
+    # It could just be that we merged other PRs and we didn't push yet
+
+    if git merge-base --is-ancestor -- "$UPSTREAM_COMMIT" "$LOCAL_BRANCH_COMMIT"; then
+        warning "Your branch is ahead of ${REMOTE}."
+        warning "You should see this warning only if you've just merged another PR and did not push yet."
+        ask_confirmation
+    else
+        error "Local branch is not up-to-date with ${REMOTE}."
+        error "Pull before merging."
+        ask_confirmation
+    fi
+fi
+
 # Sanity check: CI failed
 
 STATUS=$(curl -s "$API/commits/$COMMIT/status")
-- 
cgit v1.2.3