From c1564f164c3acee3b74593ebc2154d718db7856b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 11 May 2005 16:39:00 +0000 Subject: [PATCH] handle XmlPushParser.Parse_error exception --- helm/ocaml/cic/cicPushParser.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/helm/ocaml/cic/cicPushParser.ml b/helm/ocaml/cic/cicPushParser.ml index 4365184bb..9a0566ec2 100644 --- a/helm/ocaml/cic/cicPushParser.ml +++ b/helm/ocaml/cic/cicPushParser.ml @@ -645,6 +645,7 @@ let parse uri filename = with | Failure "int_of_string" -> parse_error ctxt "integer number expected" | Invalid_argument "bool_of_string" -> parse_error ctxt "boolean expected" + | P.Parse_error msg -> parse_error ctxt ("parse error: " ^ msg) | Parser_failure _ | Getter_failure _ as exn -> raise exn -- 2.39.2