- Reinsert line deleted per accident

diff --git a/run-tests.php b/run-tests.php
index 49d650f8eae327fdfff5fbcf49a0d5a8f6e087d9..77bfb96554a12c15ee96d912a0ed8169d7f45a06 100755 (executable)
--- a/run-tests.php
+++ b/run-tests.php
@@ -184,6 +184,7 @@ More .INIs  : " , (function_exists(\'php_ini_scanned_files\') ? str_replace("\n"
        settings2array($ini_overwrites,$info_params);
        settings2params($info_params);
        $php_info = `$php $pass_options $info_params $info_file`;
+       @unlink($info_file);
        define('TESTED_PHP_VERSION', `$php -r 'echo PHP_VERSION;'`);
 
        $unicode = `$php $pass_options $info_params -r 'echo ini_get("unicode_semantics");'`;