]> matita.cs.unibo.it Git - helm.git/commit
XmlDiff-ing of DOM trees implemented.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 22 Jul 2003 14:08:39 +0000 (14:08 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 22 Jul 2003 14:08:39 +0000 (14:08 +0000)
commit75f24bc40a8b7b1d00e6e88cb9a7b08c6551cac7
treee4a76a209083eb85e3eec1ab6f2e16a3c52be4ff
parent21bf57e0b7de37faa4991e136cf6f09cfbf4d0a3
XmlDiff-ing of DOM trees implemented.
SPECIAL FEATURE: the selection attribute of mactions are not patched.
helm/gTopLevel/.depend
helm/gTopLevel/Makefile
helm/gTopLevel/termViewer.ml
helm/gTopLevel/xmlDiff.ml [new file with mode: 0644]
helm/gTopLevel/xmlDiff.mli [new file with mode: 0644]