X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pintos-anon;a=blobdiff_plain;f=src%2Futils%2Fpintos;h=e460866719588afb40838e9fead814bc14abfeea;hp=2ebe642a5d1de310121d7f9acb2989cabb181b84;hb=8b39127d9437709ab55ad1ed7ac4fb65245fc57b;hpb=fd2a5afa946474ba0839de0e9da238dbaecbd6a5

diff --git a/src/utils/pintos b/src/utils/pintos
index 2ebe642..e460866 100755
--- a/src/utils/pintos
+++ b/src/utils/pintos
@@ -853,7 +853,7 @@ sub xsystem {
 	alarm (0);
 	&$cleanup ();
 
-	if (WIFSIGNALED ($?) && WTERMSIG ($?) == SIGVTALRM ()) {
+	if (WIFSIGNALED ($?) && WTERMSIG ($?) == SIGVTALRM_number ()) {
 	    seek (STDOUT, 0, 2);
 	    print "\nTIMEOUT after $timeout seconds of host CPU time\n";
 	    exit 0;
@@ -928,7 +928,7 @@ sub exec_setitimer {
     exit (1);
 }
 
-sub SIGVTALRM {
+sub SIGVTALRM_number {
     use Config;
     my $i = 0;
     foreach my $name (split(' ', $Config{sig_name})) {