diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/errors.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/errors.ml b/lib/errors.ml index 8982dde148..1459141d1e 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -144,5 +144,5 @@ let handled e = let fatal_error info anomaly = let msg = info ++ fnl () in pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg; - flush_all (); + Format.pp_print_flush !Pp_control.err_ft (); exit (if anomaly then 129 else 1) |