X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Futils%2Fpintos;h=920b28dfa80349f46cb7888c5f20a28a23f0f693;hb=641a6e3078a66123fb30057e2f281d6e1a6a7ca4;hp=a2168d225dc5405c1eea49bcb3e731f29f096f7c;hpb=d11a8c92f3107d4f61727130f4412608bad81854;p=pintos-anon

diff --git a/src/utils/pintos b/src/utils/pintos
index a2168d2..920b28d 100755
--- a/src/utils/pintos
+++ b/src/utils/pintos
@@ -182,7 +182,7 @@ sub run_vm {
 	    print BOCHSRC "display_library: term\n";
 	}
 	close (BOCHSRC);
-	run_command ($bin, '-q');
+	run_command_no_die ($bin, '-q');
     } elsif ($sim eq 'qemu') {
 	print "warning: qemu doesn't support --terminal\n"
 	    if $vga eq 'terminal';
@@ -273,6 +273,11 @@ sub run_command {
     die "command failed\n" if system (@_);
 }
 
+sub run_command_no_die {
+    print join (' ', @_), "\n";
+    system (@_);
+}
+
 sub search_path {
     my ($target) = @_;
     for $dir (split (':', $ENV{PATH})) {