diff options
| author | Hugo Herbelin | 2016-10-11 22:32:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-17 20:14:13 +0200 |
| commit | 9603b9996c717b52e95626ea69fe9b05a89f4738 (patch) | |
| tree | bdab5105305b2a349d8ef1a8ca837f155e0f08a2 /kernel | |
| parent | 3c4a8dffc3ad01ce170aac2043fd2e40db4449bf (diff) | |
Vernac.ml: parenthesizing a side-effect.
Moving set_formatter_out_channel where it naturally closes the
corresponding opening set_formatter_output_functions.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions