Committed Markus's patch to fixed bug 219334: [hovering] Increase target area for resizing Javadoc hovers
1 file changed