summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2022-09-27 11:42:11 +0100
committerDavid Allsopp <david.allsopp@metastack.com>2022-09-27 21:02:37 +0100
commite7115b0b1a9e5cf5632332f81e241a3d283b648d (patch)
treeb9746711aca01bd7c63948e8095bdb2bc0a2a56f
parent7c2e1e93523d9cc5b9cd6a8acf3a83a6eebe4550 (diff)
downloadocaml-e7115b0b1a9e5cf5632332f81e241a3d283b648d.tar.gz
Pass on make's -j argument to GNU parallel
-rw-r--r--testsuite/Makefile9
1 files changed, 8 insertions, 1 deletions
diff --git a/testsuite/Makefile b/testsuite/Makefile
index 1f156a68f2..e1cf40e39e 100644
--- a/testsuite/Makefile
+++ b/testsuite/Makefile
@@ -228,6 +228,13 @@ all-%: lib tools
# I chose to keep the previous behavior exactly unchanged,
# but the demangling separation is arguably nicer behavior that we might
# want to implement at the exec-one level to also have it in the 'all' target.
+
+# If make has been invoked with "-j n", pass this on to GNU parallel. parallel
+# does not support -j without an argument, hence the double-filter. Note that
+# GNU make normalises -j in $(MAKEFLAGS) so it will either be -j alone or -jn
+# (i.e. with no space).
+J_ARGUMENT = $(filter-out -j,$(filter -j%,$(MAKEFLAGS)))
+
.PHONY: parallel-%
parallel-%: lib tools
@echo | parallel >/dev/null 2>/dev/null \
@@ -239,7 +246,7 @@ parallel-%: lib tools
echo "This target requires GNU parallel.";\
exit 1)
@for dir in tests/$**; do echo $$dir; done \
- | parallel --gnu --no-notice --keep-order \
+ | parallel --gnu --no-notice --keep-order $(J_ARGUMENT) \
"$(MAKE) --no-print-directory exec-one DIR={} 2>&1" \
| tee $(TESTLOG)
@$(MAKE) report