diff options
| author | ppedrot | 2012-06-26 17:48:11 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-26 17:48:11 +0000 |
| commit | dee03ce384a75ffebca4cedf40bdbdb640ae8d8a (patch) | |
| tree | e6f8ad966decc2e41763ce2a634e294838a2c05b | |
| parent | e41469c0156f9743c51ca6677b62237569511271 (diff) | |
Fixed string width printing in string_of_ppcmds
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15493 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | lib/pp_control.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/pp_control.ml b/lib/pp_control.ml index cefd08c559..2cec00a8a3 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -82,6 +82,7 @@ let set_depth_boxes v = let get_margin () = Some (Format.pp_get_margin !std_ft ()) let set_margin v = let v = match v with None -> default_margin | Some v -> v in + Format.pp_set_margin Format.str_formatter v; Format.pp_set_margin !std_ft v; Format.pp_set_margin !deep_ft v |