From 8976834af25d8d7ddabe8ffe95decf5f8a059de6 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 6 Jan 2022 13:58:54 +0100
Subject: [PATCH] [gui] Allows to set checkbox label
---
src/plugins/gui/widget.ml | 1 +
src/plugins/gui/widget.mli | 1 +
2 files changed, 2 insertions(+)
diff --git a/src/plugins/gui/widget.ml b/src/plugins/gui/widget.ml
index 011a7587d25..fdec28d50e0 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 e208ca117ea..1a93c68e7af 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 ->
--
GitLab