diff options
Diffstat (limited to 'bin')
| -rwxr-xr-x | bin/generate-dfa-benchmark.py | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/bin/generate-dfa-benchmark.py b/bin/generate-dfa-benchmark.py index e6c3001..64f8f73 100755 --- a/bin/generate-dfa-benchmark.py +++ b/bin/generate-dfa-benchmark.py @@ -593,7 +593,8 @@ if __name__ == "__main__": if "codegen" in driver_definition and "flags" in driver_definition["codegen"]: if run_flags is None: run_flags = driver_definition["codegen"]["flags"] - run_flags.extend(opt["run"].split()) + if "run" in opt: + run_flags.extend(opt["run"].split()) runs = list( pta.dfs( |