diff options
| author | Guillaume Melquiond | 2019-11-07 19:14:44 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2019-11-07 19:14:44 +0100 |
| commit | 882e37cfa843ff7444525550e7ac3fe44b1fcecb (patch) | |
| tree | 6eff644df6493ec227cecda1b01504203ab5aab0 /ide/session.mli | |
| parent | 64ddd9ac0c34e560a0640297e2e23b6aaf074810 (diff) | |
Do not rely on the user settings but on the actual window size. (Fixes #10956)
This should fix the issue when creating new session panes. The initial
session panes, however, might still be wrongly sized, as we do not yet
know, at the time they are created, if the window manager will respect the
user settings fixing the window size.
Diffstat (limited to 'ide/session.mli')
| -rw-r--r-- | ide/session.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/session.mli b/ide/session.mli index f5d8d7c991..63ac1e6dc0 100644 --- a/ide/session.mli +++ b/ide/session.mli @@ -51,3 +51,5 @@ val kill : session -> unit val build_layout : session -> GObj.widget option * GObj.widget option * GObj.widget + +val window_size : (int * int) ref |