diff --git a/src/plugins/gui/widget.ml b/src/plugins/gui/widget.ml index 011a7587d25c304c39598f5352829a4aced8aecd..fdec28d50e0c2323b2aa40f37cf185b1d44a9aab 100644 --- a/src/plugins/gui/widget.ml +++ b/src/plugins/gui/widget.ml @@ -211,6 +211,7 @@ class checkbox ~label ?tooltip () = inherit [bool] selector false as s inherit! gobj_action button as b method! set_enabled e = s#set_enabled e ; b#set_enabled e + method set_label l = button#set_label l method! set a = s#set a ; button#set_active a initializer begin diff --git a/src/plugins/gui/widget.mli b/src/plugins/gui/widget.mli index e208ca117ead4812fb75cb93cfdd545a03f2d52c..1a93c68e7af2934c4311e8ad16908ad5d6829386 100644 --- a/src/plugins/gui/widget.mli +++ b/src/plugins/gui/widget.mli @@ -130,6 +130,7 @@ class checkbox : label:string -> ?tooltip:string -> unit -> object inherit action inherit [bool] selector + method set_label : string -> unit end class switch : ?tooltip:string -> unit ->