From b1da9a230adae91dbb4eca08a0b2a217bf15902a Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com> Date: Mon, 2 Nov 2020 12:48:11 +0100 Subject: [PATCH] Makefile: fix recursive invocation to use `$(MAKE)` Calling `make` is known-bad in many cases, but never as much as here: ``` make[2]: Nothing to be done for `pre-all'. touch theories/algebra/ofe.vo touch theories/algebra/monoid.vo touch theories/algebra/cmra.vo [...] touch theories/heap_lang/lib/array.vo make[2]: Nothing to be done for `post-all'. make[1]: *** wait: No child processes. Stop. gmake: *** [Makefile:3: all] Error 2 ``` --- Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index f34bcca55..9f262326d 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,6 @@ # Default target all: Makefile.coq - +@make -f Makefile.coq all + +@$(MAKE) -f Makefile.coq all .PHONY: all # Permit local customization @@ -9,12 +9,12 @@ all: Makefile.coq # Forward most targets to Coq makefile (with some trick to make this phony) %: Makefile.coq phony @#echo "Forwarding $@" - +@make -f Makefile.coq $@ + +@$(MAKE) -f Makefile.coq $@ phony: ; .PHONY: phony clean: Makefile.coq - +@make -f Makefile.coq clean + +@$(MAKE) -f Makefile.coq clean find theories tests exercises solutions \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true rm -f Makefile.coq .lia.cache builddep/* .PHONY: clean -- GitLab