diff options
author | Olivier Marty <olivier@oliviermarty.net> | 2017-08-07 22:28:47 +0200 |
---|---|---|
committer | Olivier Marty <olivier@oliviermarty.net> | 2017-08-08 13:24:12 +0200 |
commit | 6bb9e026d6bed7c11cf26628f3468d5ed0c31fe2 (patch) | |
tree | db2b1b0abc8edeb1221dc0a74aac970a6950e4e7 /ide/wg_Detachable.ml | |
parent | 1f46ff6db53c2ca471d9ea067d0824755b2f34da (diff) |
Set detachable windows type hint to dialog.
Windows such as Search & Replace are dialogs. For some window
managers, the hint changes how the window is displayed.
Diffstat (limited to 'ide/wg_Detachable.ml')
-rw-r--r-- | ide/wg_Detachable.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml index e5b436427..3d3a5ccb2 100644 --- a/ide/wg_Detachable.ml +++ b/ide/wg_Detachable.ml @@ -19,7 +19,7 @@ class detachable (obj : ([> Gtk.box] as 'a) Gobject.obj) = inherit GPack.box_skel (obj :> Gtk.box Gobject.obj) as super val but = GButton.button () - val win = GWindow.window () + val win = GWindow.window ~type_hint:`DIALOG () val frame = GBin.frame ~shadow_type:`NONE () val mutable detached = false val mutable detached_cb = (fun _ -> ()) |