4 files changed, 66 insertions, 20 deletions
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index e4359f703..5205350a6 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -27,9 +27,9 @@ 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 checkout -b "${BRANCH}"; then
 
-    if ! git cherry-pick -x ${RANGE}; then
+    if ! git cherry-pick -x "${RANGE}"; then
         echo "Please fix the conflicts, then exit."
         bash
         while ! git cherry-pick --continue; do
@@ -50,7 +50,7 @@ else
 
 fi
 
-if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then
+if ! git diff --exit-code HEAD "${BRANCH}" -- "*.mli"; then
     echo
     read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r
     echo
@@ -63,8 +63,8 @@ if [[ "${OPTION}" == "--stop-before-merging" ]]; then
     exit 0
 fi
 
-git merge -S --no-ff ${BRANCH} -m "${MESSAGE}"
-git branch -d ${BRANCH}
+git merge -S --no-ff "${BRANCH}" -m "${MESSAGE}"
+git branch -d "${BRANCH}"
 
 # To-Do:
 # - Support for backporting a PR before it is merged
diff --git a/dev/tools/check-overlays.sh b/dev/tools/check-overlays.sh
new file mode 100755
index 000000000..f7e05b51c
--- /dev/null
+++ b/dev/tools/check-overlays.sh
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+for f in dev/ci/user-overlays/*
+do
+    if ! ([[ $f = dev/ci/user-overlays/README.md ]] || [[ $f == *.sh ]])
+    then
+        >&2 echo "Bad overlay '$f'."
+        >&2 echo "User overlays need to have extension .sh to be picked up!"
+        exit 1
+    fi
+done
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 2f6f1af54..1c94f630f 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -4,11 +4,20 @@ set -e
 set -o pipefail
 
 API=https://api.github.com/repos/coq/coq
-OFFICIAL_REMOTE_URL="git@github.com:coq/coq"
+OFFICIAL_REMOTE_GIT_URL="git@github.com:coq/coq"
+OFFICIAL_REMOTE_HTTPS_URL="https://github.com/coq/coq"
 
-# This script depends (at least) on git and jq.
+# This script depends (at least) on git (>= 2.7) and jq.
 # It should be used like this: dev/tools/merge-pr.sh /PR number/
 
+# Set SLOW_CONF to have the confirmation output wait for a newline
+# E.g. call $ SLOW_CONF= dev/tools/merge-pr.sh /PR number/
+if [ -z ${SLOW_CONF+x} ]; then
+    QUICK_CONF="-n 1"
+else
+    QUICK_CONF=""
+fi
+
 RED="\033[31m"
 RESET="\033[0m"
 GREEN="\033[32m"
@@ -32,7 +41,7 @@ fi
 }
 
 ask_confirmation() {
-  read -p "Continue anyway? [y/N] " -n 1 -r
+  read -p "Continue anyway? [y/N] " $QUICK_CONF -r
   echo
   if [[ ! $REPLY =~ ^[Yy]$ ]]
   then
@@ -61,10 +70,12 @@ fi
 
 # Fetching PR metadata
 
-TITLE=$(curl -s "$API/pulls/$PR" | jq -r '.title')
+PRDATA=$(curl -s "$API/pulls/$PR")
+
+TITLE=$(echo "$PRDATA" | jq -r '.title')
 info "title for PR $PR is ${BLUE}$TITLE"
 
-BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label')
+BASE_BRANCH=$(echo "$PRDATA" | jq -r '.base.label')
 info "PR $PR targets branch ${BLUE}$BASE_BRANCH"
 
 CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
@@ -77,11 +88,13 @@ if [ -z "$REMOTE" ]; then
   error "please run: git branch --set-upstream-to=THE_REMOTE/$CURRENT_LOCAL_BRANCH"
   exit 1
 fi
-REMOTE_URL=$(git remote get-url "$REMOTE" --push)
-if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" -a \
-     "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then
+REMOTE_URL=$(git remote get-url "$REMOTE" --all)
+if [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}" ] && \
+   [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}.git" ] && \
+   [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_HTTPS_URL}" ] && \
+   [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_HTTPS_URL}.git" ]; then
   error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo"
-  error "that is ${BLUE}$OFFICIAL_REMOTE_URL"
+  error "that is ${BLUE}$OFFICIAL_REMOTE_GIT_URL"
   error "it points to ${BLUE}$REMOTE_URL${RESET} instead"
   ask_confirmation
 fi
@@ -105,19 +118,39 @@ if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then
   ask_confirmation
 fi;
 
+# Sanity check: the local branch is up-to-date with upstream
+
+LOCAL_BRANCH_COMMIT=$(git rev-parse HEAD)
+UPSTREAM_COMMIT=$(git rev-parse @{u})
+if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then
+
+    # Is it just that the upstream branch is behind?
+    # It could just be that we merged other PRs and we didn't push yet
+
+    if git merge-base --is-ancestor -- "$UPSTREAM_COMMIT" "$LOCAL_BRANCH_COMMIT"; then
+        warning "Your branch is ahead of ${REMOTE}."
+        warning "You should see this warning only if you've just merged another PR and did not push yet."
+        ask_confirmation
+    else
+        error "Local branch is not up-to-date with ${REMOTE}."
+        error "Pull before merging."
+        ask_confirmation
+    fi
+fi
+
 # Sanity check: CI failed
 
-STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state')
+STATUS=$(curl -s "$API/commits/$COMMIT/status")
 
-if [ "$STATUS" != "success" ]; then
-  error "CI unsuccessful on ${BLUE}$(curl -s "$API/commits/$COMMIT/status" |
+if [ "$(echo "$STATUS" | jq -r '.state')" != "success" ]; then
+  error "CI unsuccessful on ${BLUE}$(echo "$STATUS" |
     jq -r -c '.statuses|map(select(.state != "success"))|map(.context)')"
   ask_confirmation
 fi;
 
 # Sanity check: has labels named "needs:"
 
-NEEDS_LABELS=$(curl -s "$API/pulls/$PR" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)')
+NEEDS_LABELS=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)')
 if [ "$NEEDS_LABELS" != "[]" ]; then
   error "needs:something labels still present: ${BLUE}$NEEDS_LABELS"
   ask_confirmation
@@ -125,7 +158,7 @@ fi
 
 # Sanity check: has milestone
 
-MILESTONE=$(curl -s "$API/pulls/$PR" | jq -rc '.milestone.title')
+MILESTONE=$(echo "$PRDATA" | jq -rc '.milestone.title')
 if [ "$MILESTONE" = "null" ]; then
   error "no milestone set, please set one"
   ask_confirmation
@@ -133,7 +166,7 @@ fi
 
 # Sanity check: has kind
 
-KIND=$(curl -s "$API/pulls/$PR" | jq -rc '.labels | map(select(.name | match("kind:"))) | map(.name)')
+KIND=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("kind:"))) | map(.name)')
 if [ "$KIND" = "[]" ]; then
   error "no kind:something label set, please set one"
   ask_confirmation
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index c9cdee84a..a514b8866 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -5,6 +5,8 @@
 
 set -e
 
+dev/tools/check-overlays.sh
+
 if ! git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh ||
         ! git diff-index --check --cached HEAD >/dev/null 2>&1 ;
 then