diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-05 22:52:09 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-08 11:31:52 +0200 |
commit | dbf1f8200c6d5d3ddb61aa093376cb78156980e1 (patch) | |
tree | f794b67e8498bba9b2b7633e9181a566cba874e2 /tools | |
parent | 38a749767b74c1fc67d02948efd13ea8c5cbcd0b (diff) |
Adding support for bindings tags to explicit prefix/suffix rather than colors.
This is usable for no-color terminal.
For instance, a typical application in mind is the Coq-generate names
marker which can be rendered with a color if the interface supports it
and a prefix "~" if the interface does not support colors.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions