diff options
Diffstat (limited to 'ide')
-rw-r--r-- | ide/preferences.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 64327d74f..b16d45b54 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -468,7 +468,7 @@ let create_tag name default = let iter table = let tag = GText.tag ~name () in table#add tag#as_tag; - pref#connect#changed (fun _ -> set_tag tag); + ignore (pref#connect#changed (fun _ -> set_tag tag)); set_tag tag; in List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table]; |