diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml index fac1f1725dcd2e809613eec7688d33e937bf4b2c..2e3c67a9ca38abe45e53408ccef3fbf2988370be 100644 --- a/src/plugins/gui/gtk_helper.ml +++ b/src/plugins/gui/gtk_helper.ml @@ -1017,10 +1017,10 @@ let spawn_command ?(timeout=0) ?stdout ?stderr s args f = let image_menu_item ~(image:GObj.widget) ~text ~packing = let mi = GMenu.menu_item () in let box = - GPack.hbox ~spacing:2 ~border_width:0 ~packing:mi#add () + GPack.hbox ~spacing:4 ~border_width:0 ~packing:mi#add () in - box#add image; - box#add (GMisc.label ~justify:`LEFT ~xalign:0. ~xpad:0 ~text ())#coerce; + box#pack image; + box#pack (GMisc.label ~text ())#coerce; packing mi; mi