From b50a7c1642a869c581dda4cc5313bab4478fa2be Mon Sep 17 00:00:00 2001
From: Alexandre Guillemot <alexandre.guillemot@inria.fr>
Date: Thu, 6 Mar 2025 09:50:25 +0100
Subject: [PATCH] correct small bug in runtest
---
runtest.py | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/runtest.py b/runtest.py
index 883165dd..c9a28792 100644
--- a/runtest.py
+++ b/runtest.py
@@ -121,7 +121,7 @@ if not args.norun:
"memory": memory_b,
"memory error": False,
"script error": False,
- "killed manually": True,
+ "killed manually": False,
}
json.dump(info_dict, info_file, indent=2)
@@ -163,11 +163,11 @@ if not args.norun:
except:
os.killpg(os.getpgid(p.pid), signal.SIGTERM)
_, _ = p.communicate()
+ info_dict["killed manually"] = True
out_file.close()
log_file.close()
- info_dict["killed manually"] = False
info_dict["return code"] = p.returncode
info_file = open("info.json", "w")
json.dump(info_dict, info_file, indent=2)
--
GitLab