diff options
| author | Emilio Jesus Gallego Arias | 2016-06-25 18:59:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-09-30 09:44:00 +0200 |
| commit | e1f25889f88e078dac0f3b454eb16a470dd5f9ae (patch) | |
| tree | 435ddbc8b2fa093508548e0d40a391ccf6b144d0 /kernel/cbytecodes.ml | |
| parent | 6d20e4c136fb2726ec8577bdfee051ecacdf8261 (diff) | |
[pp] Remove duplicate color logger.
We use the same printing path for color and mono terminal output, thus
removing the duplicate printers which avoids problems as they don't have
to be kept in sync anymore.
We tag unconditionally but set the `pp_tag` tagger properly. This
removes IO from `Ppstyle` with IMO is the right thing to do.
Test suite passes.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions