blob: 9448400522b2c65620350dd985ff4178fe898407 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
# Include this script after a shutdown to wait until the pid file,
# stored in $pid_file, has disappered.
#--echo $pid_file
--disable_result_log
--disable_query_log
# Wait one minute
let $counter= 600;
while ($counter)
{
--error 0,1
--file_exists $pid_file
if (!$errno)
{
dec $counter;
--real_sleep 0.1
}
if ($errno)
{
let $counter= 0;
}
}
if (!$errno)
{
--die Pid file "$pid_file" failed to disappear
}
--enable_query_log
--enable_result_log
|