diff options
| author | Pierre-Marie Pédrot | 2019-11-13 15:20:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-13 15:20:06 +0100 |
| commit | dde10a9b2512ffc7e941c79bbc442c5b4b1f45f9 (patch) | |
| tree | c7e4cbb5b690aaea3a9dedfd516e252fea2ea435 /ide/session.mli | |
| parent | c45f079c52524da687dfcc9e5f5511d6e86bc537 (diff) | |
| parent | 882e37cfa843ff7444525550e7ac3fe44b1fcecb (diff) | |
Merge PR #11070: Do not rely on the user settings but on the actual window size. (Fixes #10956)
Reviewed-by: ppedrot
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 |