diff options
Diffstat (limited to 'scripts/LocalDriver.py')
| -rw-r--r-- | scripts/LocalDriver.py | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/scripts/LocalDriver.py b/scripts/LocalDriver.py index a04c03157a0..1dd6f858e34 100644 --- a/scripts/LocalDriver.py +++ b/scripts/LocalDriver.py @@ -577,6 +577,8 @@ class LocalDriver(Driver): self.runner.stopServerSide(server, current, success) except Exception as ex: failure.append(ex) + except KeyboardInterrupt: # Potentially raised by Except.py if Ctrl-C + pass sem.release() t=threading.Thread(target = stopServerSide) |