diff --git a/utils/NightlyTest.pl b/utils/NightlyTest.pl index 85dbae7f6c9..50756bf3f6e 100755 --- a/utils/NightlyTest.pl +++ b/utils/NightlyTest.pl @@ -197,7 +197,8 @@ my $BuildTime = $BuildTimeU+$BuildTimeS; # BuildTime = User+System my $BuildWallTime = GetRegexNum "^real", 1, "([0-9.]+)","$Prefix-Build-Log.txt"; my $BuildError = ""; -if (`grep '^gmake[^:]*: .*Error' $Prefix-Build-Log.txt | wc -l` + 0) { +if (`grep '^gmake[^:]*: .*Error' $Prefix-Build-Log.txt | wc -l` + 0 || + `grep '^gmake: \*\*\*.*Stop.`+0) { $BuildError = "

Build error: compilation " . "aborted

"; }