diff options
| -rw-r--r-- | driver/optmain.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/optmain.ml b/driver/optmain.ml index 7bfe26e53..71597936b 100644 --- a/driver/optmain.ml +++ b/driver/optmain.ml @@ -94,7 +94,7 @@ let main () = end; exit 0 with x -> - Format.set_formatter_output stderr; + Format.set_formatter_out_channel stderr; Opterrors.report_error x; exit 2 |