3 files changed, 110 insertions, 1 deletions
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
new file mode 100755
index 0000000000..bc6ee31916
--- /dev/null
+++ b/dev/tools/backport-pr.sh
@@ -0,0 +1,60 @@
+#!/usr/bin/env bash
+
+# Usage: git-backport <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
new file mode 100755
index 0000000000..f770004a5c
--- /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
diff --git a/dev/tools/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh
index 8159506b41..d85d651070 100755
--- a/dev/tools/should-check-whitespace.sh
+++ b/dev/tools/should-check-whitespace.sh
@@ -2,4 +2,5 @@
 
 # determine if a file has whitespace checking enabled in .gitattributes
 
-git check-attr whitespace -- "$1" | grep -q -v 'unspecified$'
+git ls-files --error-unmatch "$1" >/dev/null 2>&1 &&
+git check-attr whitespace -- "$1" | grep -q -v -e 'unset$' -e 'unspecified$'