]> matita.cs.unibo.it Git - helm.git/commitdiff
bugfix: removed spurious section "helm_registry" from save_to generated files
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 14 Jul 2005 09:14:18 +0000 (09:14 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 14 Jul 2005 09:14:18 +0000 (09:14 +0000)
helm/ocaml/registry/helm_registry.ml

index a845cb576e2017083a18230e66de0ce766295a93..8ee95ca30b646706e54c602188fed6236c5d4c55 100644 (file)
@@ -242,9 +242,9 @@ let xml_tree_of_registry registry =
     | _ -> assert false
   in
   Hashtbl.fold
-    (fun k v tree -> add_key ("helm_registry" :: (Str.split dot_RE k)) v tree)
+    (fun k v tree -> add_key ((Str.split dot_RE k)) v tree)
     registry
-    (Element ("helm_registry", [], []))
+    (Element (root_tag, [], []))
 
 let rec stream_of_xml_tree = function
   | Cdata s -> Xml.xml_cdata s