From 7d3e3f0aa5aea66a5e3c884eb0642a317d762051 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 28 Mar 2018 16:56:37 +0200
Subject: Merge script: use fetch URL for the remote.

In case the push URL has been overriden to make it fetch-only.
---
 dev/tools/merge-pr.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 20612eeb85..aa83c626e3 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -79,7 +79,7 @@ if [ -z "$REMOTE" ]; then
   error "please run: git branch --set-upstream-to=THE_REMOTE/$CURRENT_LOCAL_BRANCH"
   exit 1
 fi
-REMOTE_URL=$(git remote get-url "$REMOTE" --push)
+REMOTE_URL=$(git remote get-url "$REMOTE" --all)
 if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" ] && \
    [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then
   error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo"
-- 
cgit v1.2.3


From e332bf0d9685679f4c5415bec7681fd948921fb5 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 28 Mar 2018 18:23:48 +0200
Subject: Merge script does not warn when the remote is set to HTTPS.

This should solve Emilio's problem.
---
 dev/tools/merge-pr.sh | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'dev')

diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index aa83c626e3..337fa43a37 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -4,7 +4,8 @@ set -e
 set -o pipefail
 
 API=https://api.github.com/repos/coq/coq
-OFFICIAL_REMOTE_URL="git@github.com:coq/coq"
+OFFICIAL_REMOTE_GIT_URL="git@github.com:coq/coq"
+OFFICIAL_REMOTE_HTTPS_URL="https://github.com/coq/coq"
 
 # This script depends (at least) on git and jq.
 # It should be used like this: dev/tools/merge-pr.sh /PR number/
@@ -80,10 +81,12 @@ if [ -z "$REMOTE" ]; then
   exit 1
 fi
 REMOTE_URL=$(git remote get-url "$REMOTE" --all)
-if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" ] && \
-   [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then
+if [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}" ] && \
+   [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}.git" ] && \
+   [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_HTTPS_URL}" ] && \
+   [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_HTTPS_URL}.git" ]; then
   error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo"
-  error "that is ${BLUE}$OFFICIAL_REMOTE_URL"
+  error "that is ${BLUE}$OFFICIAL_REMOTE_GIT_URL"
   error "it points to ${BLUE}$REMOTE_URL${RESET} instead"
   ask_confirmation
 fi
-- 
cgit v1.2.3


From ff223fac386ab4d0e622d1dc03d47cff34db3311 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 8 Apr 2018 20:19:18 +0200
Subject: Document requirement to have git >= 2.7 to use the merge script.

As reported in https://github.com/coq/coq/issues/7097#issuecomment-378632415
---
 dev/tools/merge-pr.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 337fa43a37..c4ee2aa73d 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -7,7 +7,7 @@ API=https://api.github.com/repos/coq/coq
 OFFICIAL_REMOTE_GIT_URL="git@github.com:coq/coq"
 OFFICIAL_REMOTE_HTTPS_URL="https://github.com/coq/coq"
 
-# This script depends (at least) on git and jq.
+# This script depends (at least) on git (>= 2.7) and jq.
 # It should be used like this: dev/tools/merge-pr.sh /PR number/
 
 RED="\033[31m"
-- 
cgit v1.2.3


From fe3977512f18c269e82765995ee1e9ba5d6e4b43 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
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')

diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index c4ee2aa73d..60e3d739ce 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


From 6083ca1d7e654041861ffcd9a835b453717f637f Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 9 Apr 2018 14:16:52 +0200
Subject: Merge script: adds a way for confirmation to expect a newline.

This fulfils Gaetan's wish.
---
 dev/tools/merge-pr.sh | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 60e3d739ce..1c94f630f2 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -10,6 +10,14 @@ OFFICIAL_REMOTE_HTTPS_URL="https://github.com/coq/coq"
 # This script depends (at least) on git (>= 2.7) and jq.
 # It should be used like this: dev/tools/merge-pr.sh /PR number/
 
+# Set SLOW_CONF to have the confirmation output wait for a newline
+# E.g. call $ SLOW_CONF= dev/tools/merge-pr.sh /PR number/
+if [ -z ${SLOW_CONF+x} ]; then
+    QUICK_CONF="-n 1"
+else
+    QUICK_CONF=""
+fi
+
 RED="\033[31m"
 RESET="\033[0m"
 GREEN="\033[32m"
@@ -33,7 +41,7 @@ fi
 }
 
 ask_confirmation() {
-  read -p "Continue anyway? [y/N] " -n 1 -r
+  read -p "Continue anyway? [y/N] " $QUICK_CONF -r
   echo
   if [[ ! $REPLY =~ ^[Yy]$ ]]
   then
-- 
cgit v1.2.3