diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml index bd8db74a74f95a207e5698d30d1c2bdd8d9a9cb7..d6cd25ea9dc06578e7d9ee03e6f749e6a423ff10 100644 --- a/src/plugins/gui/design.ml +++ b/src/plugins/gui/design.ml @@ -847,8 +847,10 @@ class main_window () : main_window_extension_points = ~width ~height ~position:`CENTER - ~allow_shrink:true - ~allow_grow:true +(*GTK3: arguments do not exist anymore at GTK level. *) +(* ~allow_shrink:true + ~allow_grow:true +*) ~show:false () in @@ -867,7 +869,10 @@ class main_window () : main_window_extension_points = (* status bar (at bottom) *) (* toplevel_vbox->bottom_hbox-> *statusbar *) let statusbar = - GMisc.statusbar ~has_resize_grip:false ~packing:bottom_hbox#add () + GMisc.statusbar + (* GTK3: argument does not exist *) + (* ~has_resize_grip:false *) + ~packing:bottom_hbox#add () in let status_context = statusbar#new_context "messages" in