From 77c04ed416f02fa3aefeb63683ebdb70d33a3814 Mon Sep 17 00:00:00 2001 From: Florian Fischer Date: Sat, 23 Nov 2019 02:00:42 +0100 Subject: also handle json files --- merge.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/merge.py b/merge.py index f3376fa..4812c37 100755 --- a/merge.py +++ b/merge.py @@ -54,9 +54,9 @@ def main(): args = parser.parse_args() for src_save in os.listdir(args.src): - if not src_save.endswith(".save"): + if not os.path.splitext(src_save)[1] in [".json", ".save"]: continue - if src_save == "facts.save": + if src_save == "facts.save" or src_save == "facts.json": continue if args.benchmarks and not src_save[:-5] in args.benchmarks: continue @@ -70,9 +70,9 @@ def main(): print(f"Can't merge {src_save} because {os.path.basename(src_save)} not in {args.dest}") continue - src_results = load_file(src_file) + src_results = load_file(src_save) - dest_results = load_file(dest_file) + dest_results = load_file(dest_save) for alloc in src_results["allocators"]: if alloc in dest_results["allocators"]: -- cgit v1.2.3