From 32d5243a426bc09e00819bc025717c15f89aa81c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Edwin=20T=C3=B6r=C3=B6k?= Date: Thu, 13 Jun 2024 15:37:54 +0100 Subject: [PATCH] Makefile: fix compatibility with the dash shell MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github CI runs the makefile using SHELL=/bin/dash, which doesn't support SIG* names for traps. Drop the SIG prefix, which works with both `dash` and `bash`. Signed-off-by: Edwin Török --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 38c7545cc83..b2198bd5eae 100644 --- a/Makefile +++ b/Makefile @@ -59,7 +59,7 @@ test: ulimit -S -t $(TEST_TIMEOUT); \ (sleep $(TEST_TIMEOUT) && ps -ewwlyF --forest)& \ PSTREE_SLEEP_PID=$$!; \ - trap "kill $${PSTREE_SLEEP_PID}" SIGINT SIGTERM EXIT; \ + trap "kill $${PSTREE_SLEEP_PID}" INT TERM EXIT; \ timeout --foreground $(TEST_TIMEOUT2) \ dune runtest --profile=$(PROFILE) --error-reporting=twice -j $(JOBS) ifneq ($(PY_TEST), NO)