diff options
| author | klaar36 <klas.arvidsson@liu.se> | 2017-05-19 14:57:47 +0200 |
|---|---|---|
| committer | klaar36 <klas.arvidsson@liu.se> | 2017-05-19 14:57:47 +0200 |
| commit | e91e5351f64f5d0503c7971b44f3aeec704a407c (patch) | |
| tree | 449e252c0de618f04295ffc59982192129f07101 | |
| parent | b3a10d1f31095182e04fa7712268a8369e2436b1 (diff) | |
| download | pintos-rs-e91e5351f64f5d0503c7971b44f3aeec704a407c.tar.gz | |
pintos script: removed cpu kvm32 setting
| -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'; |