diff --git a/src/plugins/wp/GuiTactic.ml b/src/plugins/wp/GuiTactic.ml index cd14d8126cfd5ca69012706ae4ba04ef3ff8c631..8484deedffa91668367340b37887826381e581a7 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 ;