diff --git a/tools/buildman/builder.py b/tools/buildman/builder.py index 5addbca44e..e27a28577c 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):