diff options
Diffstat (limited to 'ide/preferences.ml')
| -rw-r--r-- | ide/preferences.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index addea9074..c4dc55972 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -386,14 +386,6 @@ let processing_color = let _ = attach_bg processing_color Tags.Script.to_process let _ = attach_bg processing_color Tags.Script.incomplete -let default_tag = { - tag_fg_color = None; - tag_bg_color = None; - tag_bold = false; - tag_italic = false; - tag_underline = false; -} - let tags = ref Util.String.Map.empty let list_tags () = !tags |