remove unused script (#2247)

This commit is contained in:
PJ Fanning 2025-09-20 16:15:02 +01:00 committed by GitHub
parent d555a86f6d
commit 343491bcdb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -1,15 +0,0 @@
#!/usr/bin/perl
use strict;
use warnings;
my $active = 0;
my $print = 0;
while (<>) {
$active = 1, next if /Generating.*\.html/;
$active = 0, next if /Genjavadoc Java API documentation successful\./;
$print = 1 if /^\[error].*error:/;
$print = 0 if /warning:/;
print if $active && $print;
}