pintos: Make sure to print buffered data at end of input.

[pintos-anon] / src / utils / pintos

diff --git a/src/utils/pintos b/src/utils/pintos
index 1abd2edc6a9055ae37788867dc022110d8310ea2..909df8391c57251f290142d134f59787590c253a 100755 (executable)
--- a/src/utils/pintos
+++ b/src/utils/pintos
@@ -819,7 +819,7 @@ sub xsystem {
            for (;;) {
                if (waitpid ($pid, WNOHANG) != 0) {
                    # Subprocess died.  Pass through any remaining data.
-                   print $buf while sysread ($in, $buf, 4096) > 0;
+                   do { print $buf } while sysread ($in, $buf, 4096) > 0;
                    last;
                }