Make stdout unbuffered while filtering output.

diff --git a/src/utils/pintos b/src/utils/pintos
index 856ebfa473ac270c70858547aabef498d7360f8d..b18693b776f6bf1679ded0b590f1c690c9500114 100755 (executable)
--- a/src/utils/pintos
+++ b/src/utils/pintos
@@ -701,12 +701,13 @@ sub xsystem {
            # Filter output.
            my ($buf) = "";
            my ($boots) = 0;
+           local ($|) = 1;
            while (waitpid ($pid, WNOHANG) == 0) {
                # Read and print out pipe data.
                my ($len) = length ($buf);
                waitpid ($pid, 0), last
                  if sysread ($in, $buf, 4096, $len) <= 0;
-               print STDOUT substr ($buf, $len);
+               print substr ($buf, $len);
 
                # Remove full lines from $buf and scan them for keywords.
                while ((my $idx = index ($buf, "\n")) >= 0) {