bin: workaround flushing issues
* bin/common_cout.cc (check_cout): Force a flush of cout if more than 20ms has elapsed since the last explicit flush. * bin/common_setup.cc (setup): Untie cin and cout if the input is not a TTY, so that cout is flush less often. * NEWS: Mention the change.
This commit is contained in:
parent
0678d1a662
commit
0c9c4be4ae
3 changed files with 44 additions and 6 deletions
8
NEWS
8
NEWS
|
|
@ -13,6 +13,14 @@ New in spot 2.1.1.dev (not yet released)
|
|||
- Fix spurious uninitialized read reported by valgrind when
|
||||
is_Kleene_star() is compiled by clang++.
|
||||
|
||||
- Using "ltlfilt some-large-file --some-costly-filter" could take
|
||||
to a lot of time before displaying the first results, because the
|
||||
output of ltlfilt is buffered: the buffer had to fill up before
|
||||
being flushed. The issue did not manifest when the input is
|
||||
standard input, because of the C++ feature that reading std::cin
|
||||
should flush std::cout; however it was well visible when reading
|
||||
from files. Flushing is now done more regularly.
|
||||
|
||||
New in spot 2.1.1 (2016-09-20)
|
||||
|
||||
Command-line tools:
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue