diff options
author | Ian Lynagh <ian@well-typed.com> | 2013-02-02 19:53:46 +0000 |
---|---|---|
committer | Ian Lynagh <ian@well-typed.com> | 2013-02-02 19:53:46 +0000 |
commit | 91aa609c448bdc04f59adf99431a12f27f6669e4 (patch) | |
tree | b7d8afaad184e00f713307f753349f540d14a712 /testsuite/timeout | |
parent | 0eed595b37d79bff5681fdfbc27bc0cd3fc1b85d (diff) | |
download | haskell-91aa609c448bdc04f59adf99431a12f27f6669e4.tar.gz |
Handle ^C better when threads are being used too
Diffstat (limited to 'testsuite/timeout')
-rw-r--r-- | testsuite/timeout/timeout.py | 85 |
1 files changed, 46 insertions, 39 deletions
diff --git a/testsuite/timeout/timeout.py b/testsuite/timeout/timeout.py index 76660a7390..6a57ac2f82 100644 --- a/testsuite/timeout/timeout.py +++ b/testsuite/timeout/timeout.py @@ -1,46 +1,53 @@ #!/usr/bin/env python -import errno -import os -import signal -import sys -import time +try: -secs = int(sys.argv[1]) -cmd = sys.argv[2] + import errno + import os + import signal + import sys + import time -def killProcess(pid): - os.killpg(pid, signal.SIGKILL) - for x in range(10): - try: - time.sleep(0.3) - r = os.waitpid(pid, os.WNOHANG) - if r == (0, 0): - os.killpg(pid, signal.SIGKILL) - else: - return - except OSError, e: - if e.errno == errno.ECHILD: - return - else: - raise e + secs = int(sys.argv[1]) + cmd = sys.argv[2] -pid = os.fork() -if pid == 0: - # child - os.setpgrp() - os.execvp('/bin/sh', ['/bin/sh', '-c', cmd]) -else: - # parent - def handler(signum, frame): - sys.stderr.write('Timeout happened...killing process...\n') - killProcess(pid) - sys.exit(99) - old = signal.signal(signal.SIGALRM, handler) - signal.alarm(secs) - (pid2, res) = os.waitpid(pid, 0) - if (os.WIFEXITED(res)): - sys.exit(os.WEXITSTATUS(res)) + def killProcess(pid): + os.killpg(pid, signal.SIGKILL) + for x in range(10): + try: + time.sleep(0.3) + r = os.waitpid(pid, os.WNOHANG) + if r == (0, 0): + os.killpg(pid, signal.SIGKILL) + else: + return + except OSError, e: + if e.errno == errno.ECHILD: + return + else: + raise e + + pid = os.fork() + if pid == 0: + # child + os.setpgrp() + os.execvp('/bin/sh', ['/bin/sh', '-c', cmd]) else: - sys.exit(res) + # parent + def handler(signum, frame): + sys.stderr.write('Timeout happened...killing process...\n') + killProcess(pid) + sys.exit(99) + old = signal.signal(signal.SIGALRM, handler) + signal.alarm(secs) + (pid2, res) = os.waitpid(pid, 0) + if (os.WIFEXITED(res)): + sys.exit(os.WEXITSTATUS(res)) + else: + sys.exit(res) + +except KeyboardInterrupt: + sys.exit(98) +except: + raise |