tests-extra: change the separator that displays the number of repetitions from :...

diff --git a/tests-extra/runtests.py b/tests-extra/runtests.py
index 8eb8ebfe9196e9468a6446ad08dc0984daa97589..d9d5ea935f70ed4ff5dcb1e7b75a698e58ca0013 100755 (executable)
--- a/tests-extra/runtests.py
+++ b/tests-extra/runtests.py
@@ -170,7 +170,7 @@ def job(job_id, tasks, results, stop):
             continue
 
         try:
-            out_dir = os.path.join(outs_dir, test, case_n.replace(" #", ":"))
+            out_dir = os.path.join(outs_dir, test, case_n.replace(" #", "__"))
             log_file = os.path.join(out_dir, "case.log")
 
             os.makedirs(out_dir, exist_ok=True)