From 9215c609bf523dcf07666c0dd2eb8732c08fb55c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 28 Jul 2003 15:15:58 +0000 Subject: [PATCH] background (deprecated) ==> mathbackground --- helm/gTopLevel/xmlDiff.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/gTopLevel/xmlDiff.ml b/helm/gTopLevel/xmlDiff.ml index 9468ccc3f..307e02ac0 100644 --- 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)) -- 2.39.2