diff --git a/tests/runtests.pl b/tests/runtests.pl index 1ab8b5e8c1..931a229771 100755 --- a/tests/runtests.pl +++ b/tests/runtests.pl @@ -850,26 +850,9 @@ if($testthis[0] ne "") { print <