diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml index 580fec0c99b6c4fde91c0ad69b574983b9ceb720..296902e97b7d60169a9a58973570dee19266c508 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) *)