From bc1fb4be47578b4da554aef69150acd77e82aba1 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 28 Nov 2017 15:05:52 +0100
Subject: Fix PR merge script.

Was still relying on the existence of user-configured /pr/.
---
 dev/tools/merge-pr.sh | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'dev')

diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index f770004a5c..63c42629cd 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -15,12 +15,12 @@ API=https://api.github.com/repos/coq/coq
 
 BASE_BRANCH=`curl -s $API/pulls/$PR | jq -r '.base.label'`
 
-COMMIT=`git rev-parse $REMOTE/pr/$PR`
+COMMIT=`git rev-parse FETCH_HEAD`
 STATUS=`curl -s $API/commits/$COMMIT/status | jq -r '.state'`
 
 if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then
   echo "Wrong base branch"
-  read -p "Bypass? [y/n] " -n 1 -r
+  read -p "Bypass? [y/N] " -n 1 -r
   echo
   if [[ ! $REPLY =~ ^[Yy]$ ]]
   then
@@ -30,7 +30,7 @@ fi;
 
 if [ $STATUS != "success" ]; then
   echo "CI status is \"$STATUS\""
-  read -p "Bypass? [y/n] " -n 1 -r
+  read -p "Bypass? [y/N] " -n 1 -r
   echo
   if [[ ! $REPLY =~ ^[Yy]$ ]]
   then
@@ -38,7 +38,7 @@ if [ $STATUS != "success" ]; then
   fi
 fi;
 
-git merge -S --no-ff $REMOTE/pr/$PR -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e
+git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e
 
 # TODO: improve this check
 if [[ `git diff $REMOTE/$CURRENT_LOCAL_BRANCH dev/ci` ]]; then
-- 
cgit v1.2.3


From 8cd635c99ae95f5d545b17df608e8276b9b5c93c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 29 Nov 2017 15:45:39 +0100
Subject: This script apparently uses bash-specific features.

---
 dev/tools/merge-pr.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 63c42629cd..0c4a79bfd3 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -1,4 +1,6 @@
-#!/bin/sh -e
+#!/usr/bin/env bash
+
+set -e
 
 # This script depends (at least) on git and jq.
 # It should be used like this: dev/tools/merge-pr.sh /PR number/
-- 
cgit v1.2.3


From f11f575b8d2db338218c8549f099dbdf3d52d7ff Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 29 Nov 2017 15:47:08 +0100
Subject: Fix usage comment.

---
 dev/tools/backport-pr.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index bc6ee31916..4c4dbe1e97 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -1,6 +1,6 @@
 #!/usr/bin/env bash
 
-# Usage: git-backport <PR number>
+# Usage: dev/tools/backport-pr.sh <PR number>
 
 set -e
 
-- 
cgit v1.2.3