10 files changed, 42 insertions, 8 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index fe8370e849..87101ecae7 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -18,7 +18,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2020-05-18-V3"
+  CACHEKEY: "bionic_coq-V2020-05-19-V33"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/.ocamlformat b/.ocamlformat
index 62e609fb55..a0d4ef6bbb 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,4 +1,4 @@
-version=0.14.0
+version=0.14.2
 profile=ocamlformat
 
 # to enable a whole directory, put "disable=false" in dir/.ocamlformat
@@ -11,4 +11,4 @@ cases-exp-indent=2
 field-space=loose
 exp-grouping=preserve
 break-cases=fit
-doc-comments-val=before
+doc-comments=before
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 51a602303a..0d2f1dfbc7 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-05-18-V3"
+# CACHEKEY: "bionic_coq-V2020-05-19-V33"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -58,7 +58,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch
 ENV COMPILER_EDGE="4.10.0" \
-    BASE_OPAM_EDGE="dune.2.5.0 dune-release.1.3.3 ocamlformat.0.14.0"
+    BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.14.2"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index fb84155392..bfb25e72dd 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
 import (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/807ca93fadd5197c2260490de0c76e500562dc05.tar.gz";
-  sha256 = "10yq8bnls77fh3pk5chkkb1sv5lbdgyk1rr2v9xn71rr1k2x563p";
+  url = "https://github.com/NixOS/nixpkgs/archive/17812e653d89c46d68b7b10e290b1c16758f4e47.tar.gz";
+  sha256 = "1zcb70dyfqc8l2ywpbvxmpfshapdi0g365m3rhmwpagqg47pnyxs";
 })
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() {
diff --git a/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst b/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst
new file mode 100644
index 0000000000..5b35090d7e
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  :cmd:Redirect now obeys the :opt:`Printing Width` and
+  :opt:`Printing Depth` flags.
+  (`#12358 <https://github.com/coq/coq/pull/12358>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/test-suite/misc/redirect_printing.out b/test-suite/misc/redirect_printing.out
new file mode 100644
index 0000000000..4f45c4d4c2
--- /dev/null
+++ b/test-suite/misc/redirect_printing.out
@@ -0,0 +1,2 @@
+nat_ind
+     : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
diff --git a/test-suite/misc/redirect_printing.sh b/test-suite/misc/redirect_printing.sh
new file mode 100755
index 0000000000..7da17407f3
--- /dev/null
+++ b/test-suite/misc/redirect_printing.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+$coqc misc/redirect_printing.v
+diff -u redirect_test.out misc/redirect_printing.out
diff --git a/test-suite/misc/redirect_printing.v b/test-suite/misc/redirect_printing.v
new file mode 100644
index 0000000000..2f9096bcb8
--- /dev/null
+++ b/test-suite/misc/redirect_printing.v
@@ -0,0 +1,2 @@
+Set Printing Width 999999.
+Redirect "redirect_test" Check nat_ind.
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 2d8734ff7f..a28d8f605b 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -404,6 +404,7 @@ let with_output_to_file fname func input =
   let channel = open_out (String.concat "." [fname; "out"]) in
   let old_fmt = !std_ft, !err_ft, !deep_ft in
   let new_ft = Format.formatter_of_out_channel channel in
+  set_gp new_ft (get_gp !std_ft);
   std_ft := new_ft;
   err_ft := new_ft;
   deep_ft := new_ft;
@@ -412,6 +413,7 @@ let with_output_to_file fname func input =
     std_ft := Util.pi1 old_fmt;
     err_ft := Util.pi2 old_fmt;
     deep_ft := Util.pi3 old_fmt;
+    Format.pp_print_flush new_ft ();
     close_out channel;
     output
   with reraise ->
@@ -419,6 +421,7 @@ let with_output_to_file fname func input =
     std_ft := Util.pi1 old_fmt;
     err_ft := Util.pi2 old_fmt;
     deep_ft := Util.pi3 old_fmt;
+    Format.pp_print_flush new_ft ();
     close_out channel;
     Exninfo.iraise reraise