diff options
| author | Jim Fehrle | 2018-11-14 18:35:50 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2019-02-26 13:23:33 -0800 |
| commit | 9736f255287a7207d00422b06de802d62b8304fe (patch) | |
| tree | 41dc987f244dfbab502a73a1deb0b68cb5680d2c /vernac/topfmt.ml | |
| parent | 4610afafcbd79f38876e528c0f30c9347648efc4 (diff) | |
Initialize styles so textual markers are used when color is not enabled
Diffstat (limited to 'vernac/topfmt.ml')
| -rw-r--r-- | vernac/topfmt.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index ed93267665..60b0bdc7e7 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -196,8 +196,8 @@ let init_tag_map styles = let default_styles () = init_tag_map (default_tag_map ()) -let parse_color_config file = - let styles = Terminal.parse file in +let parse_color_config str = + let styles = Terminal.parse str in init_tag_map styles let dump_tags () = CString.Map.bindings !tag_map |