diff options
Diffstat (limited to 'lib/pp_control.ml')
| -rw-r--r-- | lib/pp_control.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 0b886342d8..e439161251 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -89,7 +89,8 @@ let with_output_to ch = let std_ft = ref Format.std_formatter let _ = set_dflt_gp !std_ft -let err_ft = with_output_to stderr +let err_ft = ref Format.err_formatter +let _ = set_gp !err_ft deep_gp let deep_ft = with_output_to stdout let _ = set_gp deep_ft deep_gp |