diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-08 18:59:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-08 19:59:03 +0200 |
| commit | f461e7657cab9917c5b405427ddba3d56f197efb (patch) | |
| tree | 467ac699f78d0360b05174238aeb1177da892503 /ide/preferences.ml | |
| parent | 9fe0471ef0127e9301d0450aacaeb1690abb82ad (diff) | |
Removing dead code and unused opens.
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 |