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

Merge branch '5.5' into 10.0

This commit is contained in:
Vicențiu Ciorbaru
2017-01-12 03:36:45 +02:00
15 changed files with 116 additions and 5 deletions

View File

@ -870,8 +870,13 @@ max_fast_restarts=5
have_sleep=1
# close stdout and stderr, everything goes to $logging now
exec 1>&-
exec 2>&-
if expr "${-}" : '.*x' > /dev/null
then
:
else
exec 1>&-
exec 2>&-
fi
while true
do