aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-04 21:18:10 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-04 21:18:10 +0200
commit87c959542e1bed55b14d371f1be02cd60d89082c (patch)
tree890568ac965ce92bbc37273c5173928d292f33ef /vernac
parentaf19d08003173718c0f7c070d0021ad958fbe58d (diff)
parentce52387e89db6dbd5678a72a454e0d833cf7b754 (diff)
Merge PR #7416: Fix #7415. Printing Width was not applied to error messages.
Diffstat (limited to 'vernac')
-rw-r--r--vernac/topfmt.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index dbfad51a6..609dac69a 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -89,12 +89,14 @@ let set_margin v =
Format.pp_set_margin Format.str_formatter v;
Format.pp_set_margin !std_ft v;
Format.pp_set_margin !deep_ft v;
+ Format.pp_set_margin !err_ft v;
(* Heuristic, based on usage: the column on the right of max_indent
column is 20% of width, capped to 30 characters *)
let m = max (64 * v / 100) (v-30) in
Format.pp_set_max_indent Format.str_formatter m;
Format.pp_set_max_indent !std_ft m;
- Format.pp_set_max_indent !deep_ft m
+ Format.pp_set_max_indent !deep_ft m;
+ Format.pp_set_max_indent !err_ft m
(** Console display of feedback *)