]> matita.cs.unibo.it Git - helm.git/commit
Bug fixed: it could have happened that the tree structured becomes scrambled
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 28 Jul 2003 13:28:11 +0000 (13:28 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 28 Jul 2003 13:28:11 +0000 (13:28 +0000)
commit122304a548cba036c8bb3769e00276b2eb3f179d
tree77cb6091d20b030319845d99690c38ff9752c3b4
parent9abc7a37a8ec0f13ddc3e9722fd278141ccb778e
Bug fixed: it could have happened that the tree structured becomes scrambled
by the highlighting operation.
helm/gTopLevel/xmlDiff.ml