File size: 449 Bytes
eba303d
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
PID_FILE="./gradio.pid"

if [ -f "${PID_FILE}" ]; then
    PID=$(cat ${PID_FILE})
    
    if ps -p ${PID} > /dev/null
    then
        kill ${PID}
        echo "Gradio process (PID: ${PID}) has been terminated."
        
        rm ${PID_FILE}
        echo "PID file removed."
    else
        echo "No process found with PID: ${PID}. It may have already been terminated."
    fi
else
    echo "PID file does not exist. Is the backend running?"
fi