From d14e6e819c0f160bd14eac13c1827fadba352dcd Mon Sep 17 00:00:00 2001 From: Kumar Shivendu Date: Wed, 7 Aug 2024 21:21:01 +0530 Subject: [PATCH] fix CI (#181) --- tools/run_ci.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/run_ci.sh b/tools/run_ci.sh index 35cde4dc..717ef5e0 100755 --- a/tools/run_ci.sh +++ b/tools/run_ci.sh @@ -13,7 +13,7 @@ function handle_term() { echo "failed=timeout" >> $GITHUB_OUTPUT } -trap 'handle_err' ERR INT EXIT +trap 'handle_err' ERR trap 'handle_term' TERM # Script, that runs benchmark within the GitHub Actions CI environment