if a node has an xref use it for cut and paste, no matter if it have an href as well

[helm.git] / helm / matita / matitaMathView.ml

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 6074fdae75e51717d83fb9fc437cf31c3251db18..4297634c809e423c8856efb4c24d7ff7384973ad 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -272,9 +272,9 @@ object (self)
          (try Hashtbl.find ids_to_terms id with Not_found -> assert false)
 
   method private string_of_node node =
-    if node#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href_ds
-    then string_of_dom_node node
-    else self#string_of_id_node node
+    if node#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
+    then self#string_of_id_node node
+    else string_of_dom_node node
 
   method private string_of_id_node node =
     let get_id (node: Gdome.element) =