From d4b4e077488a4cbdf21b95950d149f59cc6ef0c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Mon, 4 Mar 2019 14:44:04 +0100 Subject: [PATCH] [Gui] Fixes the lablgtk3 support. --- src/plugins/gui/wbox.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/plugins/gui/wbox.ml b/src/plugins/gui/wbox.ml index b15c784631b..df6f6d12252 100644 --- a/src/plugins/gui/wbox.ml +++ b/src/plugins/gui/wbox.ml @@ -121,6 +121,10 @@ let split ~dir w1 w2 = in (splitter :> splitter) let scroll ?(hpolicy=`AUTOMATIC) ?(vpolicy=`AUTOMATIC) w = + (* Explicit conversion needed for lablgtk3, as policy_type has been extended + with another constructor but we still export the lablgtk2 type. *) + let vpolicy = (vpolicy :> Gtk.Tags.policy_type) in + let hpolicy = (hpolicy :> Gtk.Tags.policy_type) in let scrolled = GBin.scrolled_window ~vpolicy ~hpolicy () in scrolled#add_with_viewport w#coerce ; new Wutil.gobj_widget scrolled -- GitLab