merged in all changes done to the trunk up to Aug 28

[pintos-anon] / src / utils / pintos

diff --git a/src/utils/pintos b/src/utils/pintos
index a62b1923bd9008f4d3c611a0a2fbb6546105e22a..d42669c7a198cae14c261b58c18245afd3024ebf 100755 (executable)
--- a/src/utils/pintos
+++ b/src/utils/pintos
@@ -585,8 +585,11 @@ panic: action=fatal
 user_shortcut: keys=ctrlaltdel
 EOF
     print BOCHSRC "gdbstub: enabled=1\n" if $debug eq 'gdb';
-    print BOCHSRC "clock: sync=", $realtime ? 'realtime' : 'none',
-      ", time0=0\n";
+    if ($realtime) {
+       print BOCHSRC "clock: sync=realtime\n";
+    } else {
+       print BOCHSRC "clock: sync=none, time0=0\n";
+    }
     print BOCHSRC "ata1: enabled=1, ioaddr1=0x170, ioaddr2=0x370, irq=15\n"
       if @disks > 2;
     print_bochs_disk_line ("ata0-master", $disks[0]);