Catch errors like: make[2]: *** No rule to make target '/usr/lib64/libhdf5.so.1.8...

diff --git a/index.php b/index.php
index 35cbe0dd36cf1aee2ceca889f8e33b674e0f1478..906294b94144c80e4942a4fda30849451ccf0f10 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)/i", $s)) {
+               } elseif (preg_match("/(?:undefined reference to|recipe for target '.*?' failed|make\[.*:.* Stop\.$)/i", $s)) {
                        $first_cut = true;
                        $err_count++;
                        $toc_elem = "error $err_count";