diff options
Diffstat (limited to 'lib/xml_parser.ml')
| -rw-r--r-- | lib/xml_parser.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml index 81fefd8805..108e226783 100644 --- a/lib/xml_parser.ml +++ b/lib/xml_parser.ml @@ -166,7 +166,9 @@ let error_of_exn xparser = function | NoMoreData -> NodeExpected | Internal_error e -> e | Xml_lexer.Error e -> convert e - | e -> raise e + | e -> + (*let e = Errors.push e in: We do not record backtrace here. *) + raise e let do_parse xparser = try |