1
0
mirror of https://github.com/MariaDB/server.git synced 2025-12-24 11:21:21 +03:00

merge 55178,55413,56383

This commit is contained in:
Bjorn Munch
2010-09-10 09:58:26 +02:00
5 changed files with 50 additions and 6 deletions

View File

@@ -684,6 +684,13 @@ sub process_opts_file {
next;
}
$value= mtr_match_prefix($opt, "--testcase-timeout=");
if ( defined $value ) {
# Overrides test case timeout for this test
$tinfo->{'case-timeout'}= $value;
next;
}
# Ok, this was a real option, add it
push(@{$tinfo->{$opt_name}}, $opt);
}