diff options
author | Daniel Friesel <daniel.friesel@uos.de> | 2020-08-18 15:50:46 +0200 |
---|---|---|
committer | Daniel Friesel <daniel.friesel@uos.de> | 2020-08-18 15:50:46 +0200 |
commit | eddecfcc02ab11b05881e49673a8a8027ae640bf (patch) | |
tree | d495a310bad9237ad886368454946bf71fb430fd | |
parent | 1d9bbd0ec9fdc2ed63630137602207260b13285b (diff) |
generate-dfa-benchmark: only set run flags when set
-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( |