From 651b1293c32512947cd2df62d09a26d2c32e9eba Mon Sep 17 00:00:00 2001
From: Paul Gauthier <aider@paulg.org>
Date: Mon, 26 Jun 2023 10:51:06 -0700
Subject: [PATCH] tweaks

---
 scripts/benchmark.py | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)
 mode change 100644 => 100755 scripts/benchmark.py

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():