Makefile: fix compatibility with the dash shell

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 <[email protected]>
edwintorok · Jun 13, 2024 · 32d5243 · 32d5243
1 parent 65dc11e
commit 32d5243
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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)