6 files changed, 88 insertions, 24 deletions
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index 4c4dbe1e9..e4359f703 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -1,10 +1,11 @@
 #!/usr/bin/env bash
 
-# Usage: dev/tools/backport-pr.sh <PR number>
+# Usage: dev/tools/backport-pr.sh <PR number> [--stop-before-merging]
 
 set -e
 
 PRNUM=$1
+OPTION=$2
 
 if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then
     echo "PR #${PRNUM} does not exist."
@@ -49,6 +50,19 @@ else
 
 fi
 
+if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then
+    echo
+    read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r
+    echo
+    if [[ ! $REPLY =~ ^[Yy]$ ]]; then
+        exit 1
+    fi
+fi
+
+if [[ "${OPTION}" == "--stop-before-merging" ]]; then
+    exit 0
+fi
+
 git merge -S --no-ff ${BRANCH} -m "${MESSAGE}"
 git branch -d ${BRANCH}
 
diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh
index 1c578c05c..9e4c8661d 100755
--- a/dev/tools/check-eof-newline.sh
+++ b/dev/tools/check-eof-newline.sh
@@ -1,9 +1,14 @@
 #!/usr/bin/env bash
 
-if [ -z "$(tail -c 1 "$1")" ]
-then
-    exit 0
-else
-    echo "No newline at end of file $1!"
-    exit 1
-fi
+CODE=0
+for f in "$@"; do
+    if git ls-files --error-unmatch "$f" >/dev/null 2>&1 && \
+           git check-attr whitespace -- "$f" | grep -q -v -e 'unset$' -e 'unspecified$' && \
+           [ -n "$(tail -c 1 "$f")" ]
+    then
+        echo "No newline at end of file $f!"
+        CODE=1
+    fi
+done
+
+exit "$CODE"
diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py
new file mode 100755
index 000000000..beb26d910
--- /dev/null
+++ b/dev/tools/github-check-prs.py
@@ -0,0 +1,47 @@
+#!/usr/bin/env python3
+
+# Requires PyGithub https://pypi.python.org/pypi/PyGithub, for instance
+# debian package: python3-github
+# nix: nix-shell -p python3 python3Packages.PyGithub --run ./github-check-rebase.py
+from github import Github
+import argparse
+
+REPO = "coq/coq"
+REBASE_LABEL="needs: rebase"
+
+parser = argparse.ArgumentParser()
+parser.add_argument("--token-file", type=argparse.FileType('r'))
+args = parser.parse_args()
+
+if args.token_file is None:
+    token = input("Github access token: ").strip()
+else:
+    token = args.token_file.read().rstrip("\n")
+    args.token_file.close()
+
+if token == "":
+    print ("Warning: using the GitHub API without a token")
+    print ("We may run into rate limit issues")
+    g = Github()
+else:
+    g = Github(token)
+
+repo = g.get_repo(REPO)
+
+for pull in repo.get_pulls():
+    # if conflicts then dirty
+    # otherwise blocked (because I have no rights)
+    dirty = pull.mergeable_state == "dirty"
+    labelled = False
+    for label in repo.get_issue(pull.number).get_labels():
+        if label.name == REBASE_LABEL:
+            labelled = True
+    if labelled and not dirty:
+        print ("PR #" + str(pull.number) + " is not dirty but is labelled")
+        print ("("+ pull.html_url +")")
+    elif dirty and not labelled:
+        print ("PR #" + str(pull.number) + " is dirty and not labelled")
+        print ("("+ pull.html_url +")")
+    else:
+        # give some feedback so the user can see we didn't crash
+        print ("PR #" + str(pull.number) + " OK")
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 0c4a79bfd..9f24960ff 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -9,18 +9,18 @@ set -e
 
 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
+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'`
+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'`
+COMMIT=$(git rev-parse FETCH_HEAD)
+STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state')
 
-if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then
+if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then
   echo "Wrong base branch"
   read -p "Bypass? [y/N] " -n 1 -r
   echo
@@ -30,7 +30,7 @@ if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then
   fi
 fi;
 
-if [ $STATUS != "success" ]; then
+if [ "$STATUS" != "success" ]; then
   echo "CI status is \"$STATUS\""
   read -p "Bypass? [y/N] " -n 1 -r
   echo
@@ -40,10 +40,10 @@ if [ $STATUS != "success" ]; then
   fi
 fi;
 
-git merge -S --no-ff FETCH_HEAD -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
+if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then
   echo "******************************************"
   echo "** WARNING: does this PR have overlays? **"
   echo "******************************************"
diff --git a/dev/tools/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh
deleted file mode 100755
index d85d65107..000000000
--- a/dev/tools/should-check-whitespace.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/usr/bin/env bash
-
-# determine if a file has whitespace checking enabled in .gitattributes
-
-git ls-files --error-unmatch "$1" >/dev/null 2>&1 &&
-git check-attr whitespace -- "$1" | grep -q -v -e 'unset$' -e 'unspecified$'
diff --git a/dev/tools/sudo-apt-get-update.sh b/dev/tools/sudo-apt-get-update.sh
new file mode 100755
index 000000000..f8bf6bed4
--- /dev/null
+++ b/dev/tools/sudo-apt-get-update.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+(sudo apt-get update "$@" 2>&1 || echo 'E: update failed') | tee /tmp/apt.err
+! grep -q '^\(E:\|W: Failed to fetch\)' /tmp/apt.err || exit $?