From 30518988c47fa7a12fdabb743c27d3b172393d41 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Fri, 4 Jan 2019 15:59:28 +0100 Subject: [PATCH] [gui] remove obsolete attribute of statusbar (See [this discussion](https://github.com/garrigue/lablgtk/issues/2#issuecomment-451203335) upstream for more information) --- src/plugins/gui/design.ml | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml index 580fec0c99b..296902e97b7 100644 --- a/src/plugins/gui/design.ml +++ b/src/plugins/gui/design.ml @@ -865,12 +865,7 @@ class main_window () : main_window_extension_points = in (* status bar (at bottom) *) (* toplevel_vbox->bottom_hbox-> *statusbar *) - let statusbar = - GMisc.statusbar - (* GTK3: using this argument leads to a crash. *) - (*~has_resize_grip:false *) - ~packing:bottom_hbox#add () - in + let statusbar = GMisc.statusbar ~packing:bottom_hbox#add () in let status_context = statusbar#new_context "messages" in (* progress bar (at bottom) *) -- GitLab