aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/checker.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index aec3e3282..a23ca8f4f 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -380,8 +380,10 @@ let init_feedback_listener () =
let pp_loc fmt loc = let open Loc in match loc with
| None -> fprintf fmt ""
| Some loc ->
- fprintf fmt "File \"%s\", line %d, characters %d-%d:@\n"
- loc.fname loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in
+ let where =
+ match loc.fname with InFile f -> f | ToplevelInput -> "Toplevel input" in
+ fprintf fmt "\"%s\", line %d, characters %d-%d:@\n"
+ where loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in
let checker_feed (fb : Feedback.feedback) = let open Feedback in
match fb.contents with
| Processed -> ()