ghc-dup: 76660a739056a9ff762f6f2afa36f8920c9a2dde
1: #!/usr/bin/env python
2:
3: import errno
4: import os
5: import signal
6: import sys
7: import time
8:
9: secs = int(sys.argv[1])
10: cmd = sys.argv[2]
11:
12: def killProcess(pid):
13: os.killpg(pid, signal.SIGKILL)
14: for x in range(10):
15: try:
16: time.sleep(0.3)
17: r = os.waitpid(pid, os.WNOHANG)
18: if r == (0, 0):
19: os.killpg(pid, signal.SIGKILL)
20: else:
21: return
22: except OSError, e:
23: if e.errno == errno.ECHILD:
24: return
25: else:
26: raise e
27:
28: pid = os.fork()
29: if pid == 0:
30: # child
31: os.setpgrp()
32: os.execvp('/bin/sh', ['/bin/sh', '-c', cmd])
33: else:
34: # parent
35: def handler(signum, frame):
36: sys.stderr.write('Timeout happened...killing process...\n')
37: killProcess(pid)
38: sys.exit(99)
39: old = signal.signal(signal.SIGALRM, handler)
40: signal.alarm(secs)
41: (pid2, res) = os.waitpid(pid, 0)
42: if (os.WIFEXITED(res)):
43: sys.exit(os.WEXITSTATUS(res))
44: else:
45: sys.exit(res)
46:
Generated by git2html.