2025-02-04 14:34:25 +00:00
|
|
|
#!/bin/bash
|
|
|
|
|
|
|
|
|
2025-02-10 12:52:21 +00:00
|
|
|
# wait <pid> in bash only works for processes that are direct children to the calling
|
|
|
|
# shell. This script is more general purpose.
|
2025-02-04 14:34:25 +00:00
|
|
|
wait_pid() {
|
|
|
|
local pid=$1
|
|
|
|
local max_attempts=100 # 100 * 0.1 seconds = 10 seconds
|
|
|
|
local attempt=0
|
|
|
|
local sleep_time=0.1
|
|
|
|
|
|
|
|
while [ $attempt -lt $max_attempts ]; do
|
|
|
|
if [[ "$OSTYPE" == "msys"* || "$OSTYPE" == "cygwin"* ]]; then
|
|
|
|
# Windows approach
|
|
|
|
if ! tasklist | grep -q $pid; then
|
|
|
|
echo "Process has ended"
|
|
|
|
return 0
|
|
|
|
fi
|
|
|
|
else
|
|
|
|
# Linux/macOS approach
|
|
|
|
if ! kill -0 $pid 2>/dev/null; then
|
|
|
|
echo "Process has ended"
|
|
|
|
return 0
|
|
|
|
fi
|
|
|
|
fi
|
|
|
|
|
|
|
|
sleep $sleep_time
|
|
|
|
attempt=$((attempt + 1))
|
|
|
|
done
|
|
|
|
|
|
|
|
echo "Timeout: Process $pid did not end within 10 seconds"
|
|
|
|
return 1
|
|
|
|
}
|
|
|
|
|
|
|
|
# Usage
|
|
|
|
if [ $# -eq 0 ]; then
|
|
|
|
echo "Usage: $0 <PID>"
|
|
|
|
exit 1
|
|
|
|
fi
|
|
|
|
|
|
|
|
wait_pid $1
|
|
|
|
exit $?
|