From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 16 Apr 2002 11:11:39 +0000 (+0000)
Subject: Removed the patch to avoid a bug of gmetadom.
X-Git-Tag: V_0_3_0_debian_8~151
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c74012ddc6f92b87c2279e277b0aa3203dfbd0ac

Removed the patch to avoid a bug of gmetadom.
---

diff --git a/helm/gTopLevel/xml2Gdome.ml b/helm/gTopLevel/xml2Gdome.ml
index 43a2fc7dd..55041995d 100644
--- a/helm/gTopLevel/xml2Gdome.ml
+++ b/helm/gTopLevel/xml2Gdome.ml
@@ -8,11 +8,8 @@ let document_of_xml (domImplementation : Gdome.domImplementation) strm =
     | _ -> assert false
   in
    let document =
-(*CSC: erroraccio bruttissimo in gmetadom!!! *)
-    new Gdome.document (
     domImplementation#createDocument ~namespaceURI:None
      ~qualifiedName:(Gdome.domString root_name) ~doctype:None
-    )
    in
    let rec aux (node : Gdome.node) =
     parser