From 38c9acbaa680e21598b61b9a3144cf2883bedb08 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 6 Jan 2022 13:59:43 +0100
Subject: [PATCH] [wp] Allows to update checkbox label
---
src/plugins/wp/GuiTactic.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/wp/GuiTactic.ml b/src/plugins/wp/GuiTactic.ml
index cd14d8126cf..8484deedffa 100644
--- a/src/plugins/wp/GuiTactic.ml
+++ b/src/plugins/wp/GuiTactic.ml
@@ -89,7 +89,7 @@ class checkbox
begin
Wutil.on enabled button#set_visible ;
Wutil.on tooltip button#set_tooltip ;
- ignore title ;
+ Wutil.on title button#set_label ;
ignore filter ;
ignore vmin ;
ignore vmax ;
--
GitLab