1
0
mirror of https://github.com/MariaDB/server.git synced 2025-07-29 05:21:33 +03:00

Merge 10.1 into 10.2

This commit is contained in:
Marko Mäkelä
2019-01-24 14:43:29 +02:00
23 changed files with 397 additions and 61 deletions

View File

@ -5270,6 +5270,7 @@ sub server_need_restart {
exists $server->{'restart_opts'})
{
my $use_dynamic_option_switch= 0;
delete $server->{'restart_opts'};
if (!$use_dynamic_option_switch)
{
mtr_verbose_restart($server, "running with different options '" .