diff options
| author | Hugo Herbelin | 2018-11-19 15:45:05 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-19 08:40:19 +0000 |
| commit | 05e15386fad28f138e6e889c421242c60b9cb39a (patch) | |
| tree | 1377138a93a361186fdcf2c20d94001e4afd586e /plugins/syntax/string_notation.mli | |
| parent | 97f973000a11e667b0d5faef9264f4e681bbd8e1 (diff) | |
CoqIDE: Now calling destroy signal via widget_signals.
Thanks to J. Garrigue for the hint.
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions