|
@@ -31,7 +31,6 @@ function patchDir(string $base, string $dir): int
|
31
|
31
|
$patched = preg_replace('/\):\s*(\?[a-zA-Z]+|void)\s*\n/', ") /*:$1*/\n", $patched);
|
32
|
32
|
$patched = preg_replace('/private const/', "/*private*/ const", $patched);
|
33
|
33
|
if ($patched && $patched != $original) {
|
34
|
|
- echo "$filename\n";
|
35
|
34
|
file_put_contents($filename, $patched);
|
36
|
35
|
$count++;
|
37
|
36
|
}
|
|
@@ -50,7 +49,7 @@ function patch(string $base, array $dirs)
|
50
|
49
|
$end = microtime(true);
|
51
|
50
|
$time = ($end - $start) * 1000;
|
52
|
51
|
if ($count) {
|
53
|
|
- echo sprintf("%d files patched in %d ms\n", $count, $time);
|
|
52
|
+ fwrite(STDERR, sprintf("%d files patched in %d ms\n", $count, $time));
|
54
|
53
|
}
|
55
|
54
|
}
|
56
|
55
|
|