diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-11 22:32:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-17 20:14:13 +0200 |
| commit | 9603b9996c717b52e95626ea69fe9b05a89f4738 (patch) | |
| tree | bdab5105305b2a349d8ef1a8ca837f155e0f08a2 /toplevel/coqloop.ml | |
| parent | 3c4a8dffc3ad01ce170aac2043fd2e40db4449bf (diff) | |
Vernac.ml: parenthesizing a side-effect.
Moving set_formatter_out_channel where it naturally closes the
corresponding opening set_formatter_output_functions.
Diffstat (limited to 'toplevel/coqloop.ml')
| -rw-r--r-- | toplevel/coqloop.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 08c3fe205..ea7539fce 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -308,7 +308,6 @@ let do_vernac () = else Feedback.msg_error (str"There is no ML toplevel.") | any -> let any = CErrors.push any in - Format.set_formatter_out_channel stdout; let msg = print_toplevel_error any ++ fnl () in pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg; Format.pp_print_flush !Pp_control.std_ft () |