From d471ff49c43a1b03278dd1c520b8b4564b75c8dd Mon Sep 17 00:00:00 2001 From: Dilum Aluthge Date: Thu, 11 Aug 2022 00:45:53 -0400 Subject: [PATCH] If the `timeout` option is provided on the command line, the `Timer` should use that value (#88) --- src/BugReporting.jl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/BugReporting.jl b/src/BugReporting.jl index f851c4c..1e69218 100644 --- a/src/BugReporting.jl +++ b/src/BugReporting.jl @@ -186,7 +186,7 @@ function rr_record(julia_cmd::Cmd, julia_args...; rr_flags=default_rr_record_fla end if timeout > 0 - @async Timer(2) do timer + @async Timer(timeout) do timer istaskdone(t1) || Base.throwto(t1, InterruptException()) end end