Catch more error messages.

diff --git a/index.php b/index.php
index 906294b94144c80e4942a4fda30849451ccf0f10..14a11ae0d7dc44b73ded970d942891c871064e3c 100644 (file)
--- a/index.php
+++ b/index.php
@@ -393,7 +393,7 @@ function dump_log($tail)
                        $toc_elem = "error $err_count";
                        $err_elem = $s;
                        $s = "<span class=error id=error-$err_count>$s</span>";
-               } elseif (preg_match("/(?:undefined reference to|recipe for target '.*?' failed|make\[.*:.* Stop\.$)/i", $s)) {
+               } elseif (preg_match("/(?:undefined reference to|recipe for target '.*?' failed|compilation terminated|make\[.*:.* (Stop\.$|Error))/i", $s)) {
                        $first_cut = true;
                        $err_count++;
                        $toc_elem = "error $err_count";