diff options
Diffstat (limited to 'src/utils/pintos')
| -rwxr-xr-x | src/utils/pintos | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/utils/pintos b/src/utils/pintos index 989bb5f..546b152 100755 --- a/src/utils/pintos +++ b/src/utils/pintos @@ -496,8 +496,8 @@ sub run_qemu { # Using '-gdb tcp::$dport' instead. push (@cmd, '-gdb', "tcp::$dport", '-S') if $debug eq 'gdb'; # push (@cmd, '-p', $dport); # replaced by above +# push (@cmd, '-singlestep'); push (@cmd, '-m', $mem); - push (@cmd, '-cpu', 'kvm32'); # klaar@ida 2015-05-07 push (@cmd, '-net', 'none'); push (@cmd, '-serial', 'stdio') if $serial && $vga ne 'none'; push (@cmd, '-S') if $debug eq 'monitor'; |