diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-11 15:55:50 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-11 15:55:50 +0100 |
| commit | ecf15647873e390171d6a62f9c28162424cb5a65 (patch) | |
| tree | 273eed085500028d3469a8585e0a611d6550cf6b /plugins/ltac/pptactic.mli | |
| parent | a77f3a3e076e273af35ad520cae2eef0e3552811 (diff) | |
| parent | d313cb4ca64dcf77a09c03e615845397e61c3bbe (diff) | |
Merge PR #6270: [toplevel] Properly redirect stdout on `Redirect` vernac.
Diffstat (limited to 'plugins/ltac/pptactic.mli')
0 files changed, 0 insertions, 0 deletions