diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-11-28 11:16:33 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-28 11:16:33 +0100 |
commit | f303ed9fb26797b9ec7d172fe583e7ee607ae441 (patch) | |
tree | 5271c2aeb0bc05b668d8180327cbe728b455d77a | |
parent | 24adb2ee00b860f4550d05bd38dde4a284bcd7bc (diff) | |
parent | 486c10572776e5d8afcc92fa9e2a0844879ca1a5 (diff) |
Merge PR #6259: Add PR merge script.
-rwxr-xr-x | dev/tools/merge-pr.sh | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh new file mode 100755 index 000000000..f770004a5 --- /dev/null +++ b/dev/tools/merge-pr.sh @@ -0,0 +1,48 @@ +#!/bin/sh -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 $REMOTE/pr/$PR` +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 $REMOTE/pr/$PR -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 + echo "******************************************" + echo "** WARNING: does this PR have overlays? **" + echo "******************************************" +fi |