From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 dev/tools/merge-pr.sh | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100755 dev/tools/merge-pr.sh

(limited to 'dev/tools/merge-pr.sh')

diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
new file mode 100755
index 00000000..9f24960f
--- /dev/null
+++ b/dev/tools/merge-pr.sh
@@ -0,0 +1,50 @@
+#!/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/
+
+#TODO: check arguments and show usage if relevant
+
+PR=$1
+
+CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
+REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote")
+git fetch "$REMOTE" "refs/pull/$PR/head"
+
+API=https://api.github.com/repos/coq/coq
+
+BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label')
+
+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
+  echo
+  if [[ ! $REPLY =~ ^[Yy]$ ]]
+  then
+    exit 1
+  fi
+fi;
+
+if [ "$STATUS" != "success" ]; then
+  echo "CI status is \"$STATUS\""
+  read -p "Bypass? [y/N] " -n 1 -r
+  echo
+  if [[ ! $REPLY =~ ^[Yy]$ ]]
+  then
+    exit 1
+  fi
+fi;
+
+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 --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then
+  echo "******************************************"
+  echo "** WARNING: does this PR have overlays? **"
+  echo "******************************************"
+fi
-- 
cgit v1.2.3