aboutsummaryrefslogtreecommitdiff
path: root/ide/wg_Tooltip.ml
AgeCommit message (Expand)Author
2013-08-19Tooltips can be augmented with custom widgets, still not clickablegareuselesinge
2013-08-12Setting tooltip font monospace.ppedrot
2013-04-25Fix: tooltip correctly handles the absence of info (empty string)gareuselesinge
2013-04-25Coqide: Globalization feedback (proof of concept)gareuselesinge