diff options
| author | Hugo Herbelin | 2018-11-11 13:26:37 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-11-11 15:44:10 +0100 |
| commit | 35a11a5567d660e545ad39c03b9bef39c26380ba (patch) | |
| tree | 61b24dbedb220be58369c1028e9c1e1a4f024a83 /dev/ci/ci-plugin-tutorial.sh | |
| parent | 3ccc9a89de9a2d5b81dae82c7815ba077f998135 (diff) | |
CoqIDE: ensure that the configuration box is not hidden by the main window.
We do it by passing the name of the main window in the "parent"
option. Formerly, the window could be hidden but nevertheless blocking
any action on the main window. With the change, it can be moved
aside, but never hidden by the main window.
Tested on MacOS X.
Diffstat (limited to 'dev/ci/ci-plugin-tutorial.sh')
0 files changed, 0 insertions, 0 deletions