X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pintos-anon;a=blobdiff_plain;f=src%2Futils%2Fpintos;h=88bd3adc1c12a662dff6a7e0430581f0f1d6da76;hp=94132052b30e4b22feba396b0f58b8b57b928a2c;hb=0fd3a243b790dd1cfc9e0a40c57dddde56cf344d;hpb=ed04361f6ec91e4f0db1550c2cc487a461b2d17b

diff --git a/src/utils/pintos b/src/utils/pintos
index 9413205..88bd3ad 100755
--- a/src/utils/pintos
+++ b/src/utils/pintos
@@ -409,8 +409,11 @@ log: bochsout.txt
 panic: action=fatal
 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_bochs_disk_line ("ata0-master", 0);
     print_bochs_disk_line ("ata0-slave", 1);
     if (defined ($disks_by_iface[2]{FILE_NAME})