diff --git a/scripts/run.py b/scripts/run.py index 8ae177a..a6fb878 100644 --- a/scripts/run.py +++ b/scripts/run.py @@ -27,6 +27,8 @@ def run(args): try: while locality_process.poll() is None: time.sleep(0.5) + except KeyboardInterrupt: + pass finally: if locality_process.poll() is None: locality_process.terminate()