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

Merge branch '10.0' into 10.1

This commit is contained in:
Vicențiu Ciorbaru
2017-09-19 12:06:50 +03:00
193 changed files with 43208 additions and 2979 deletions

View File

@@ -742,8 +742,7 @@ sub run_test_server ($$$) {
# Repeat test $opt_repeat number of times
my $repeat= $result->{repeat} || 1;
# Don't repeat if test was skipped
if ($repeat < $opt_repeat && $result->{'result'} ne 'MTR_RES_SKIPPED')
if ($repeat < $opt_repeat)
{
$result->{retries}= 0;
$result->{rep_failures}++ if $result->{failures};
@@ -5818,7 +5817,7 @@ sub debugger_arguments {
$$exe= $debugger;
}
elsif ( $debugger =~ /windbg/ )
elsif ( $debugger =~ /windbg|vsjitdebugger/ )
{
# windbg exe arg1 .. argn