make dotty field optional in json

Summary:
public
The "dotty" field in json reports is only used when reporting retain cycles. It
makes sense not to emit it by default (when it's `None`).

Reviewed By: akotulski

Differential Revision: D2891320

fb-gh-sync-id: 54292a9
master
Jules Villard 9 years ago committed by facebook-github-bot-5
parent e11395d199
commit cbb8810e2c

@ -188,8 +188,7 @@ let error_desc_to_plain_string error_desc =
pp_to_string pp ()
let error_desc_to_dotty_string error_desc =
let dotty_opt = Localise.error_desc_get_dotty error_desc in
match dotty_opt with Some s -> s | None -> ""
Localise.error_desc_get_dotty error_desc
let error_desc_to_xml_string error_desc =
let pp fmt () = F.fprintf fmt "%a" Localise.pp_error_desc error_desc in

@ -31,7 +31,7 @@ type jsonbug = {
key : int;
qualifier_tags : tag_value_record list;
hash : int;
dotty : string;
?dotty : string option;
?infer_source_loc: loc option;
}

Loading…
Cancel
Save