diff --git a/scripts/benchmark.py b/scripts/benchmark.py old mode 100644 new mode 100755 index 60857ded8..3dd801a9d --- a/scripts/benchmark.py +++ b/scripts/benchmark.py @@ -1,3 +1,5 @@ +#!/usr/bin/env python + import argparse import datetime import json @@ -107,7 +109,10 @@ def main(): print("ERROR: will not delete dir that does not look like original tests", dirname) return - dest = dirname.parent / "OLD" / (now + dirname.name) + dest = dirname.parent / "OLD" / dirname.name + if dest.exists(): + dest = dirname.parent / "OLD" / (now + dirname.name) + dirname.rename(dest) if not dirname.exists():