4 files changed, 40 insertions, 2 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index d5c6096100..801e29ac95 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -179,6 +179,11 @@ but if you wish to save more time you can skip the job by setting
 
 This means you will need to change its value when the Docker image
 needs to be updated. You can do so for a single pipeline by starting
-it through the web interface.
+it through the web interface. Here is a direct link that you can use
+to trigger such a build:
+`https://gitlab.com/coq/coq/pipelines/new?var[SKIP_DOCKER]=false&ref=pr-XXXXX`.
+Note that this link will give a 404 error if you are not logged in or
+a member of the Coq organization on GitLab.  To request to join the
+Coq organization, go to https://gitlab.com/coq to request access.
 
 See also [`docker/README.md`](docker/README.md).
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5f7d0b5789..19ba9de245 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -239,6 +239,13 @@
 : "${elpi_hb_CI_ARCHIVEURL:=${elpi_hb_CI_GITURL}/archive}"
 
 ########################################################################
+# Engine-Bench
+########################################################################
+: "${engine_bench_CI_REF:=master}"
+: "${engine_bench_CI_GITURL:=https://github.com/mit-plv/engine-bench}"
+: "${engine_bench_CI_ARCHIVEURL:=${engine_bench_CI_GITURL}/archive}"
+
+########################################################################
 # fcsl-pcm
 ########################################################################
 : "${fcsl_pcm_CI_REF:=master}"
diff --git a/dev/ci/ci-engine_bench.sh b/dev/ci/ci-engine_bench.sh
new file mode 100755
index 0000000000..fda7649f88
--- /dev/null
+++ b/dev/ci/ci-engine_bench.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download engine_bench
+
+( cd "${CI_BUILD_DIR}/engine_bench" && make coq && make coq-perf-Sanity )
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index ce64aebdc7..82e4bd1e1e 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -49,10 +49,26 @@ ask_confirmation() {
   fi
 }
 
+curl_paginate_array() {
+  # as per https://developer.github.com/v3/guides/traversing-with-pagination/#changing-the-number-of-items-received, GitHub will never give us more than 100
+  url="$1?per_page=100"
+  # we keep fetching pages until the response is below the per-page limit (possibly 0 elements)
+  page=1
+  while true; do
+    response="$(curl -s "${url}&page=${page}")"
+    echo "${response}"
+    if [ "$(jq 'length' <<< "$response")" -lt 100 ]; then # done
+      break
+    fi
+    page=$(($page + 1))
+  done | jq '[.[]]' # we concatenate the arrays
+}
+
 check_util jq
 check_util curl
 check_util git
 check_util gpg
+check_util grep
 
 # command line parsing
 
@@ -70,6 +86,8 @@ fi
 
 # Fetching PR metadata
 
+# The main API call returns a dict/object, not an array, so we don't
+# bother paginating
 PRDATA=$(curl -s "$API/pulls/$PR")
 
 TITLE=$(echo "$PRDATA" | jq -r '.title')
@@ -203,7 +221,7 @@ fi
 # Generate commit message
 
 info "Fetching review data"
-reviews=$(curl -s "$API/pulls/$PR/reviews")
+reviews=$(curl_paginate_array "$API/pulls/$PR/reviews")
 msg="Merge PR #$PR: $TITLE"
 
 has_state() {