Merge of the V7_3_new_exportation branch.

[helm.git] / helm / gTopLevel / xml2Gdome.ml

diff --git a/helm/gTopLevel/xml2Gdome.ml b/helm/gTopLevel/xml2Gdome.ml
index 8c6298d09026b93e7443f5014c6c68caa28b26d1..c4e9445ebbe74a583225e7ea25ac3ef8de5b9558 100644 (file)
--- a/helm/gTopLevel/xml2Gdome.ml
+++ b/helm/gTopLevel/xml2Gdome.ml
@@ -27,6 +27,8 @@ let document_of_xml (domImplementation : Gdome.domImplementation) strm =
  let module G = Gdome in
  let module X = Xml in
   let root_name,root_attributes,root_content =
+   ignore (Stream.next strm) ; (* to skip the <?xml ...?> declaration *)
+   ignore (Stream.next strm) ; (* to skip the DOCTYPE declaration *)
    match Stream.next strm with
       X.Empty(n,l) -> n,l,[<>]
     | X.NEmpty(n,l,c) -> n,l,c