diff options
| author | Hugo Herbelin | 2018-11-19 01:02:59 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-19 08:40:20 +0000 |
| commit | 0f91d7fbbaf790e84b30f60410ddae4cbbd9c3eb (patch) | |
| tree | 2b9028cf451687512c43b0dbaadc1a15857b346c /ide/wg_ScriptView.ml | |
| parent | ae3fa5305a034015a894e3fa6f6cea27c4138b9a (diff) | |
CoqIDE: Using Grid instead of Table.
This is not mandatory for gtk+3 since it is deprecated from only gtk
3.4. This would be needed for gtk+4 though.
Diffstat (limited to 'ide/wg_ScriptView.ml')
0 files changed, 0 insertions, 0 deletions