diff options
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/backport-pr.sh | 60 | ||||
| -rwxr-xr-x | dev/tools/merge-pr.sh | 12 |
2 files changed, 67 insertions, 5 deletions
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh new file mode 100755 index 0000000000..4c4dbe1e97 --- /dev/null +++ b/dev/tools/backport-pr.sh @@ -0,0 +1,60 @@ +#!/usr/bin/env bash + +# Usage: dev/tools/backport-pr.sh <PR number> + +set -e + +PRNUM=$1 + +if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then + echo "PR #${PRNUM} does not exist." + exit 1 +fi + +SIGNATURE_STATUS=$(git log master --grep "Merge PR #${PRNUM}" --format="%G?") +git log master --grep "Merge PR #${PRNUM}" --format="%GG" +if [[ "${SIGNATURE_STATUS}" != "G" ]]; then + echo + read -p "Merge commit does not have a good (valid) signature. Bypass? [y/N] " -n 1 -r + echo + if [[ ! $REPLY =~ ^[Yy]$ ]]; then + exit 1 + fi +fi + +BRANCH=backport-pr-${PRNUM} +RANGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%P" | sed 's/ /../') +MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merge/Backport/') + +if git checkout -b ${BRANCH}; then + + if ! git cherry-pick -x ${RANGE}; then + echo "Please fix the conflicts, then exit." + bash + while ! git cherry-pick --continue; do + echo "Please fix the conflicts, then exit." + bash + done + fi + git checkout - + +else + + echo + read -p "Skip directly to merging phase? [y/N] " -n 1 -r + echo + if [[ ! $REPLY =~ ^[Yy]$ ]]; then + exit 1 + fi + +fi + +git merge -S --no-ff ${BRANCH} -m "${MESSAGE}" +git branch -d ${BRANCH} + +# To-Do: +# - Support for backporting a PR before it is merged +# - Automatically backport all PRs in the "Waiting to be backported" column using a command like: +# $ curl -s -H "Authorization: token ${GITHUB_TOKEN}" -H "Accept: application/vnd.github.inertia-preview+json" https://api.github.com/projects/columns/1358120/cards | jq -r '.[].content_url' | grep issue | sed 's/^.*issues\/\([0-9]*\)$/\1/' | tac +# (The ID of the column must first be obtained through https://api.github.com/repos/coq/coq/projects then https://api.github.com/projects/819866/columns.) +# - Then move each of the backported PR to the subsequent columns automatically as well... diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index f770004a5c..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/ @@ -15,12 +17,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 +32,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 +40,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 |