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 /Makefile.build | |
| 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 'Makefile.build')
0 files changed, 0 insertions, 0 deletions