From 4f43abbdb698bcc608afb6d8e270aee64d4f2a74 Mon Sep 17 00:00:00 2001
From: Damien Doligez <damien.doligez@inria.fr>
Date: Tue, 13 Feb 2024 17:05:24 +0100
Subject: [PATCH] display more details in case of a failed test

---
 test/TOOLS/time_one_test | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/test/TOOLS/time_one_test b/test/TOOLS/time_one_test
index 5498321d..c9685c80 100755
--- a/test/TOOLS/time_one_test
+++ b/test/TOOLS/time_one_test
@@ -3,6 +3,18 @@
 FILE="$1"
 TOOLDIR="$2"
 
-exec "$TOOLDIR"/do_one_test "$FILE" "$TOOLDIR/separator" \
+"$TOOLDIR"/do_one_test "$FILE" "$TOOLDIR/separator" \
                             "$FILE.out" "$FILE.err" \
                             >"$FILE.out" 2>"$FILE.err"
+retcode=$?
+case $retcode in
+    0) ;;
+    *)
+        printf "failed with return code %d\n" $retcode
+        printf "#### stdout:\n"
+        cat "$FILE.out"
+        printf "#### stderr:\n"
+        cat "$FILE.err"
+        exit $retcode
+        ;;
+esac