diff options
| author | Hugo Herbelin | 2018-11-22 01:10:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-17 07:42:46 +0100 |
| commit | 06c4f33eedc14bfdf7c6a603ff87feccb57c32f5 (patch) | |
| tree | 8ad27815e8402f298f67a404a0aa56a147dc039f /kernel/nativecode.mli | |
| parent | 7e155688331c8f004f34950da67108d7284e4e56 (diff) | |
CoqIDE: Restoring configuration of default width/height of main window.
Also removing dead code about show_toolbar: this is governed by an
item of the view menu rather than by the preference panel since
aa357d601 (Dec 2003).
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions