diff options
| author | Hugo Herbelin | 2018-11-11 15:13:45 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-11-11 15:44:10 +0100 |
| commit | a60461fdc0453a32451221d22e906ea74a0341e5 (patch) | |
| tree | 21e211449ed49034b887cde376d23bc60b1871bf /dev/ci/ci-plugin_tutorial.sh | |
| parent | 008354e71473ecdae0ca34dd5af951c4a4ae18dc (diff) | |
CoqIDE: pass the parent window to all methods liable to open a question box.
This is to ensure that the corresponding question boxes remains in
front of the main window, consistently with the fact that they are
blocking actions on the main window.
Diffstat (limited to 'dev/ci/ci-plugin_tutorial.sh')
0 files changed, 0 insertions, 0 deletions