diff --git a/share/analysis-scripts/summary.py b/share/analysis-scripts/summary.py index 0b2fc9c9fbaa6724922aae8db70db6d3c45db6f1..77da19d6aa3c66b25adf4bb189f005e339556cb0 100755 --- a/share/analysis-scripts/summary.py +++ b/share/analysis-scripts/summary.py @@ -55,11 +55,11 @@ def list_targets(dir): targets = res.stdout.split() res = [] for target in targets: - if target.endswith(".eva") or target.endswith(".parse"): - res.append(dir + "/" + target) + target_path = f"{dir}/{target}" + if os.path.isdir(target_path): + res.append(target_path) else: - res += [dir + "/" + t for t in list_targets(target)] - print(f"list_targets returning: {res}") + raise OperationException(f"target is not a directory: {target_path}") return res def clone_frama_c(clonedir, hash):