Files
zulip/tools/stop_run_dev
K.Kanakhin cb1d61cae0 run-dev: Add pid file to development server.
- Add pid file of development processes group, which allows to
  manage development processes group with os utils. Also it allows to
  kill subprocesses  when parent process was closed incorrectly.
- Add tool 'stop_dev_server' to stop development server by pid file.

Fixes #1547
2017-02-02 21:07:03 -08:00

31 lines
676 B
Python
Executable File

#!/usr/bin/env python
from __future__ import print_function
import os
import signal
import sys
os.chdir(os.path.join(os.path.dirname(__file__), '..'))
pid_file_path = os.path.join(os.path.join(os.getcwd(), 'var/run/run_dev.pid'))
try:
with open(pid_file_path, 'r') as pid_file:
try:
pid = int(pid_file.read())
except ValueError:
print('PID value is not an integer!')
sys.exit(1)
except Exception as e:
print("PID file can't be opened!")
print(e)
sys.exit(1)
# Kill development server process group.
try:
os.killpg(pid, signal.SIGTERM)
except OSError as e:
print(e)
sys.exit(1)
print("Done")