diff options
Diffstat (limited to 'otherlibs/labltk/browser/viewer.ml')
| -rw-r--r-- | otherlibs/labltk/browser/viewer.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/otherlibs/labltk/browser/viewer.ml b/otherlibs/labltk/browser/viewer.ml index bebd908c7..e5943f096 100644 --- a/otherlibs/labltk/browser/viewer.ml +++ b/otherlibs/labltk/browser/viewer.ml @@ -212,7 +212,7 @@ let view_defined modlid :env = with Not_found -> () | Env.Error err -> let tl, tw, finish = Jg_message.formatted title:"Error!" () in - Env.report_error err; + Env.report_error Format.std_formatter err; finish () let close_all_views () = |