Commit 48e626fc authored by POTTIER Francois's avatar POTTIER Francois
Browse files use a shell command that prints TIMEOUT only when appropriate and

preserves the exit code.
parent 34cd9df2
......@@ -214,7 +214,9 @@ let menhir (impose_timeout : bool) base flags =
(* We must use a [system] action. *)
let command =
"timeout %d %%{bin:menhir}%s || echo 'TIMEOUT after %d seconds.'"
"timeout %d %%{bin:menhir}%s || \
(status=$?; if (( $status == 124 )) ; then \
echo 'TIMEOUT after %d seconds.' ; fi; exit $status)"
(show_list (menhir_args base flags))
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment