diff options
| -rw-r--r-- | driver/main.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/main.ml b/driver/main.ml index 97d659a94..5bf380864 100644 --- a/driver/main.ml +++ b/driver/main.ml @@ -81,7 +81,7 @@ let main () = end; exit 0 with x -> - Format.set_formatter_output stderr; + Format.set_formatter_out_channel stderr; Errors.report_error x; exit 2 |