Spaces:
Running
Running
| 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 | |