Be smarter about dealing with make failures.

diff --git a/grading/lib/Pintos/Grading.pm b/grading/lib/Pintos/Grading.pm
index 30ac7101493b473bf96a316f0268e986f64581fb..f29dc05f7c9ae494682c0ea49eb0f99ea2a5d22d 100644 (file)
--- a/grading/lib/Pintos/Grading.pm
+++ b/grading/lib/Pintos/Grading.pm
@@ -422,7 +422,14 @@ sub run_pintos {
 sub grade_test {
     # Read test output.
     my ($outfile) = "output/$test/run.out";
-    die "$outfile: missing test output file (make failed?)" if ! -e $outfile;
+    if (! -e $outfile) {
+       if (-s "output/$test.make.err") {
+           # make failed.
+           $details{$test} = snarf ("output/$test.make.err");
+           return "make failed.  Error messages at end of file.";
+       }
+       die "$outfile: missing test output file";
+    }
     my (@output) = snarf ($outfile);
 
     # If there's a function "grade_$test", use it to evaluate the output.