From 0ca18665e5e44ad386eeeb929b28353865b6b839 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 8 Feb 2021 15:46:55 +0100
Subject: [PATCH] [Gui] remove unerasable-optional-argument warning related to
menu_manager
---
src/plugins/gui/design.ml | 2 +-
src/plugins/gui/menu_manager.ml | 2 +-
src/plugins/gui/menu_manager.mli | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index c5a986d5802..21ade2a5af1 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1034,7 +1034,7 @@ class main_window () : main_window_extension_points =
let m =
new Menu_manager.menu_manager
~packing:(toplevel_vbox#pack ~expand:false ~fill:false ~from:`START)
- ~host:(self :> Gtk_helper.host)
+ (self :> Gtk_helper.host)
in
menu_manager <- Some m;
m
diff --git a/src/plugins/gui/menu_manager.ml b/src/plugins/gui/menu_manager.ml
index 5d835aabd1c..af195e70150 100644
--- a/src/plugins/gui/menu_manager.ml
+++ b/src/plugins/gui/menu_manager.ml
@@ -112,7 +112,7 @@ let add_submenu container ~pos label =
external set_menu : Obj.t -> unit = "ige_mac_menu_set_menu_bar"
*)
-class menu_manager ?packing ~host:(_:Gtk_helper.host) =
+class menu_manager ?packing (_:Gtk_helper.host) =
let menubar = GMenu.menu_bar ?packing () in
(* let () = set_menu (Obj.field (Obj.repr ((menubar)#as_widget)) 1) in *)
let factory = new GMenu.factory menubar in
diff --git a/src/plugins/gui/menu_manager.mli b/src/plugins/gui/menu_manager.mli
index dba70f9279c..22f5cba0dc5 100644
--- a/src/plugins/gui/menu_manager.mli
+++ b/src/plugins/gui/menu_manager.mli
@@ -113,7 +113,7 @@ end
(** How to handle a Frama-C menu.
@since Boron-20100401 *)
-class menu_manager: ?packing:(GObj.widget -> unit) -> host:Gtk_helper.host ->
+class menu_manager: ?packing:(GObj.widget -> unit) -> Gtk_helper.host ->
object
(** {2 API for plug-ins} *)
--
GitLab