diff options
| author | Gaëtan Gilbert | 2019-07-21 17:10:46 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-21 17:10:46 +0200 |
| commit | 9b929e16b1123674c737c1cef2002f5a3c3f2d39 (patch) | |
| tree | d2cb7b69d44eecd265089f1512f7afb2b4db7c0c /plugins | |
| parent | f1206ec5d6c6d7f557ec6802e64b41d82fc806f8 (diff) | |
Dune: do not use with-outputs-to for shims
We only want stdout, so if there's something in stderr it will both
make a wrong output and make it harder to debug.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions