diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-28 19:17:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:47:13 +0100 |
| commit | eda304d2f0531b8fa088a2d71d369d4482f29ed2 (patch) | |
| tree | ceb1d3681536d077a435eae276af3df84b2fb765 /plugins/ltac/pptactic.mli | |
| parent | f1c5e2ce2a4515a7c90c5ca22aa6eff22dd2f5ff (diff) | |
[ide] ide_slave doesnt't need to capture stdout
The miscellaneous `msg_*` cleanup patches have finally enforced this
invariant.
Diffstat (limited to 'plugins/ltac/pptactic.mli')
0 files changed, 0 insertions, 0 deletions