Flush output from timing script.

pull/44975/head
Matt Clay 6 years ago
parent 857a553fa1
commit 771768966f

@ -8,3 +8,4 @@ start = time.time()
for line in sys.stdin:
seconds = time.time() - start
sys.stdout.write('%02d:%02d %s' % (seconds // 60, seconds % 60, line))
sys.stdout.flush()

Loading…
Cancel
Save