diff options
| author | Guillaume Melquiond | 2015-12-31 17:02:00 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-12-31 17:02:00 +0100 |
| commit | 5319465eb1eaf89410dac96cd14b14b9b95601e7 (patch) | |
| tree | b52306041b4351e6a01984d391da3a82af82ec11 /interp | |
| parent | 1a157442dff4bfa127af467c49280e79889acde7 (diff) | |
| parent | d3bc575c498ae09ad1003405d17a9d5cfbcf3cbf (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/dumpglob.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index c18ceecaba..c7d3da653c 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -139,12 +139,15 @@ let interval loc = loc1, loc2-1 let dump_ref loc filepath modpath ident ty = - if !glob_output = Feedback then + match !glob_output with + | Feedback -> Pp.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty)) - else + | NoGlob -> () + | _ when not (Loc.is_ghost loc) -> let bl,el = interval loc in dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n" bl el filepath modpath ident ty) + | _ -> () let dump_reference loc modpath ident ty = let filepath = Names.DirPath.to_string (Lib.library_dp ()) in |