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: