diff --git a/ptests/ptests.ml b/ptests/ptests.ml index 2483e59e8fd46452db5cf24dba01f512b9e9d1b2..f402cb79bd2826a48a03216e55bc84ea8a9c3433 100644 --- a/ptests/ptests.ml +++ b/ptests/ptests.ml @@ -1110,6 +1110,16 @@ let command_string command = in let res = Filename.sanitize (log_prefix ^ ".res.log") in let command_string = command_string ^ " >" ^ res in + let command_string = + match command.timeout with + | "" -> command_string + | s -> + Printf.sprintf + "%s; if test $? -eq 124; then \ + echo 'TIMEOUT (%s); ABORTING EXECUTION' > %s; \ + fi" + command_string s (Filename.sanitize stderr) + in let command_string = match filter with | None -> command_string | Some filter ->