hover: add preference to disable showing it
User should be able to choose to not show hovers (like for Java editor).
Leave a comment
on 2012-11-22 11:16 *
By Vlad Dumitrescu
Milestone changed from sprint #37 to sprint #36
Milestone changed from sprint #37 to sprint #36