diff options
Diffstat (limited to 'src/reference_tree.ml')
| -rw-r--r-- | src/reference_tree.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/reference_tree.ml b/src/reference_tree.ml index 84f1934..bdc1cdc 100644 --- a/src/reference_tree.ml +++ b/src/reference_tree.ml @@ -161,6 +161,7 @@ let data_from_xml d x = let rec insert_from_xml basepath reftree xml = match xml with + | Xml.Element ("syntaxVersion", _, _) -> reftree | Xml.Element (_, _, _) -> let props = find_xml_child "properties" xml in let data = |