diff options
author | 2016-06-28 16:52:46 +0200 | |
---|---|---|
committer | 2017-03-21 15:47:13 +0100 | |
commit | f1c5e2ce2a4515a7c90c5ca22aa6eff22dd2f5ff (patch) | |
tree | 2a295b6855f0bab21922ea8621ee3ce680e5e7dd /tactics | |
parent | 28d3bb3c8bddc63d038d8d55a34c928675fa9f7b (diff) |
[ide] Use "log via feedback".
We remove the custom logger handler in ide_slave, and handle everything
via feedback. This is an experimental patch but it seems to bring quite
a bit of cleanup and a more uniform handling to messaging.
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions