aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coqchk
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-26 15:04:02 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-26 16:00:31 +0100
commit2919e4a927a4574a28012ae4ba9523e01fed1360 (patch)
tree41dec3a4166b257c4deed07c08ce4fb361684e4c /test-suite/coqchk
parent3bcd71163e5645aa6a0becedfbb2768389469d25 (diff)
coqchk: flush the pp buffer from time to time
Diffstat (limited to 'test-suite/coqchk')
0 files changed, 0 insertions, 0 deletions