diff options
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 |