From 343491bcdb3963ad167f3e3289f01d3eeb53e27b Mon Sep 17 00:00:00 2001 From: PJ Fanning Date: Sat, 20 Sep 2025 16:15:02 +0100 Subject: [PATCH] remove unused script (#2247) --- scripts/find-javadoc-error.pl | 15 --------------- 1 file changed, 15 deletions(-) delete mode 100755 scripts/find-javadoc-error.pl diff --git a/scripts/find-javadoc-error.pl b/scripts/find-javadoc-error.pl deleted file mode 100755 index 12bede4313..0000000000 --- a/scripts/find-javadoc-error.pl +++ /dev/null @@ -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; -} -