diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-07 10:50:55 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-06-14 19:31:10 +0200 |
| commit | 2e0e2d662421c5c1ec3415da9ca94054e0cc2898 (patch) | |
| tree | 644e2a515ce8bbbfe24d51836a48c803aeabcffb /checker/check_stat.ml | |
| parent | 4a5b6f10b55597e0a0d27ec34fa4f914cfcbc6e8 (diff) | |
Fix for bug #4784
We revert the change of flushing strategy in the toplevel.
PR #179 introduced a different flushing in toplevel, but it creates
problems as new lines appear when Set Printing Width is large and proof
general complains, see bugzilla#4784. The use of `flush_all` also
produces missing output.
IMO, this is a pitfall of the current setup, in particular, `Format` is
used without enclosing expressions in top-level boxes, as required. This
results in undefined behavior and fragile printing such as this bug
exemplifies.
Test suite passes.
Diffstat (limited to 'checker/check_stat.ml')
0 files changed, 0 insertions, 0 deletions