1
0
mirror of https://github.com/MariaDB/server.git synced 2025-08-08 11:22:35 +03:00

Fix for make dist

This commit is contained in:
monty@hundin.mysql.fi
2001-09-29 15:37:53 +03:00
parent 5293d2ea2d
commit 12aa7e5e84
4 changed files with 7 additions and 5 deletions

View File

@@ -118,7 +118,7 @@ case "$mode" in
'stop')
# Stop daemon. We use a signal here to avoid having to know the
# root password.
if test -f "$pid_file"
if test -s "$pid_file"
then
mysqld_pid=`cat $pid_file`
echo "Killing mysqld with pid $mysqld_pid"