Committed Markus's patch to fixed bug 216868: [hovering] Rich hovers API polish
1 file changed