From: Ben Pfaff <blp@cs.stanford.edu>
Date: Wed, 5 Apr 2006 19:33:33 +0000 (+0000)
Subject: Warn if timeout used with debugger.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pintos-anon;a=commitdiff_plain;h=6863628ceb049af4dcb60d9d04286d2b5b25ef94

Warn if timeout used with debugger.
Thanks to Alicia Chen <achen530@stanford.edu> for question.
---

diff --git a/src/utils/pintos b/src/utils/pintos
index eee6384..0c1f34d 100755
--- 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).