diff --git a/tools/local_run.py b/tools/local_run.py index 7454d124..259197ed 100644 --- a/tools/local_run.py +++ b/tools/local_run.py @@ -49,5 +49,5 @@ else: os.execvpe( sys.executable, - ['-Wall', spath] + args, + ['-Wall', '-s', spath] + args, env)