X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Futils%2Fpintos;h=d42669c7a198cae14c261b58c18245afd3024ebf;hb=8fff557107b6a3efec0000ce98904450c1de3648;hp=a62b1923bd9008f4d3c611a0a2fbb6546105e22a;hpb=e81af6fff9570e6f3f2b13bb9ad54cc17f25aa50;p=pintos-anon

diff --git a/src/utils/pintos b/src/utils/pintos
index a62b192..d42669c 100755
--- 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]);