diff options
| author | Pierre-Marie Pédrot | 2018-12-18 10:13:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-18 10:13:58 +0100 |
| commit | 74313ad1ce4693ed197ada385edbdec2b7ce5a81 (patch) | |
| tree | d322ce64ba75bdc29654d39ef12d60002cf957ec /doc/plugin_tutorial/tuto1/src | |
| parent | c115e6703b7a59cbe5f4851a7e673f54323f3e12 (diff) | |
| parent | 06c4f33eedc14bfdf7c6a603ff87feccb57c32f5 (diff) | |
Merge PR #9178: CoqIDE: Restoring configuration of default width/height of main window.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src')
0 files changed, 0 insertions, 0 deletions