Increase the size of the border of selected nodes in the html trace.
authorKim Nguyễn <kn@lri.fr>
Sun, 18 Aug 2013 10:19:08 +0000 (12:19 +0200)
committerKim Nguyễn <kn@lri.fr>
Sun, 18 Aug 2013 10:19:08 +0000 (12:19 +0200)

No differences found