From 882e37cfa843ff7444525550e7ac3fe44b1fcecb Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 7 Nov 2019 19:14:44 +0100
Subject: 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.
---
 ide/session.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'ide/session.mli')

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
-- 
cgit v1.2.3