diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-28 16:07:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-28 16:12:18 +0100 |
| commit | d313cb4ca64dcf77a09c03e615845397e61c3bbe (patch) | |
| tree | d5a9b91fc4c3e56b9e64b8e8a6cd6e4cad42e3a9 /install.sh | |
| parent | f303ed9fb26797b9ec7d172fe583e7ee607ae441 (diff) | |
[toplevel] Properly redirect stdout on `Redirect` vernac.
Fixes #6130, it was a silly omission from a previous output
refactoring.
We redirect all channels as this was the implied semantics of the old
command.
Diffstat (limited to 'install.sh')
0 files changed, 0 insertions, 0 deletions