diff options
author | 2016-12-05 17:56:22 +0100 | |
---|---|---|
committer | 2017-03-21 15:51:39 +0100 | |
commit | 3fc02bb2034a648c9c27b76a9e7b4e02a78e55b9 (patch) | |
tree | cf3856edc9b24a75d30f465e6e29a42962329a4a /Makefile.dev | |
parent | a8ec2dc5c330ded1ba400ef202c57e68d2533312 (diff) |
[pp] Move terminal-specific tagging to the toplevel.
Previously, tags were associated to terminal styles, which doesn't make
sense on terminal-free pretty printing scenarios.
This commit moves tag interpretation to the toplevel terminal handling
module `Topfmt`.
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions