background (deprecated) ==> mathbackground

diff --git a/helm/gTopLevel/xmlDiff.ml b/helm/gTopLevel/xmlDiff.ml
index 9468ccc3f68a96bd1a16a7db85f4448828969a1c..307e02ac0db8c325fd45b0b5ebb3158a89118a3c 100644 (file)
--- a/helm/gTopLevel/xmlDiff.ml
+++ b/helm/gTopLevel/xmlDiff.ml
@@ -53,7 +53,7 @@ let highlight_node ?(color="yellow") (doc: Gdome.document) (n: Gdome.node) =
     ~namespaceURI:(Some (Gdome.domString mathmlns))
     ~qualifiedName:(Gdome.domString "m:mstyle")
   in
-   highlighter#setAttribute ~name:(Gdome.domString "background")
+   highlighter#setAttribute ~name:(Gdome.domString "mathbackground")
     ~value:(Gdome.domString color) ;
    highlighter#setAttributeNS
     ~namespaceURI:(Some (Gdome.domString xmldiffns))