Warn if timeout used with debugger.

[pintos-anon] / src / utils / pintos

diff --git a/src/utils/pintos b/src/utils/pintos
index eee638407f0507521bf8624a5cf8e64ae26fefa3..0c1f34d54aab6c79d1a7f6ec7cb81e0380c0545d 100755 (executable)
--- a/src/utils/pintos
+++ b/src/utils/pintos
@@ -85,6 +85,9 @@ sub parse_command_line {
     $sim = "bochs" if !defined $sim;
     $debug = "none" if !defined $debug;
     $vga = "window" if !defined $vga;
+
+    print "warning: -T or --timeout should not be used with --$debug\n"
+      if defined ($timeout) && $debug ne 'none';
 }
 
 # usage($exitcode).