commit | fc41bf46acaccb3da8d0588b7e1bbcfebc6442f6 | [log] [download] |
---|---|---|
author | nicm <nicm> | Thu Oct 25 15:13:38 2018 +0000 |
committer | nicm <nicm> | Thu Oct 25 15:13:38 2018 +0000 |
tree | 35eb7a9295fd36e29661b20a506551565ced9d16 | |
parent | 9feb35b7c4007966bf19cdb57b904e373da2d247 [diff] |
Add a "terminal" colour which can be used instead of "default" in style options for the terminal default colour, bypassing any inheritance from other options. Prompted by a discussion with abieber@.