diff options
| author | Hugo Herbelin | 2018-11-12 07:52:44 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-19 08:40:17 +0000 |
| commit | 1e76c9f840135d6445e89090fcd3c6c073115a15 (patch) | |
| tree | 95f96a2cab081bd2c2d161c25bf8133c3fde1369 /ide/wg_ScriptView.mli | |
| parent | f3ccaf7b094bce98b309263aac862413bbb86b2d (diff) | |
CoqIDE: Replacing Tooltips with gtk+3 compliant Tooltip.
Diffstat (limited to 'ide/wg_ScriptView.mli')
0 files changed, 0 insertions, 0 deletions