| Age | Commit message (Expand) | Author |
|---|---|---|
| 2013-08-19 | Tooltips can be augmented with custom widgets, still not clickable | gareuselesinge |
| 2013-08-12 | Setting tooltip font monospace. | ppedrot |
| 2013-04-25 | Fix: tooltip correctly handles the absence of info (empty string) | gareuselesinge |
| 2013-04-25 | Coqide: Globalization feedback (proof of concept) | gareuselesinge |
