diff --git a/run-tests.php b/run-tests.php index 16241c08cc6..edfab1f57ad 100755 --- a/run-tests.php +++ b/run-tests.php @@ -1583,6 +1583,10 @@ escape: kill_children($workerProcs); error("Could not find worker stdout in array of worker stdouts, THIS SHOULD NOT HAPPEN."); } + if (feof($workerSock)) { + kill_children($workerProcs); + error("Worker $i died unexpectedly"); + } while (false !== ($rawMessage = fgets($workerSock))) { // work around fgets truncating things if (($rawMessageBuffers[$i] ?? '') !== '') {