diff options
| author | Gaëtan Gilbert | 2020-05-21 14:47:45 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-05-21 14:47:45 +0200 |
| commit | 0aedb0c8464d7f84a6fda9ed24290a8341fe8322 (patch) | |
| tree | 21f2c1d6d2d56243b10297cc26ca8e6648060eca /doc | |
| parent | 7c17979b38bebbc6730cb1b3edf5fa1329f2f001 (diff) | |
| parent | fb0caf14daff2e433dfc33ca564d49b26f7e8fb4 (diff) | |
Merge PR #12358: [topfmt] Set formatter + flush fix
Reviewed-by: JasonGross
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst | 5 |
1 files changed, 5 insertions, 0 deletions
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). |