diff options
Diffstat (limited to 'tools/buildman/builder.py')
| -rw-r--r-- | tools/buildman/builder.py | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tools/buildman/builder.py b/tools/buildman/builder.py index 5addbca44e9..e27a28577c2 100644 --- a/tools/buildman/builder.py +++ b/tools/buildman/builder.py @@ -12,6 +12,7 @@ import os import re import Queue import shutil +import signal import string import sys import threading @@ -282,11 +283,17 @@ class Builder: ignore_lines = ['(make.*Waiting for unfinished)', '(Segmentation fault)'] self.re_make_err = re.compile('|'.join(ignore_lines)) + # Handle existing graceful with SIGINT / Ctrl-C + signal.signal(signal.SIGINT, self.signal_handler) + def __del__(self): """Get rid of all threads created by the builder""" for t in self.threads: del t + def signal_handler(self, signal, frame): + sys.exit(1) + def SetDisplayOptions(self, show_errors=False, show_sizes=False, show_detail=False, show_bloat=False, list_error_boards=False, show_config=False): |