From 65c4598c755e256e5fd7a6b1d381b643b05aeeb2 Mon Sep 17 00:00:00 2001 From: Paul Eggert Date: Fri, 8 May 2015 13:52:05 -0700 Subject: [PATCH] Prefer '$(MAKE)' to 'make' * Makefile (check_public, check_time_t_alternatives) (typecheck): Use '$(MAKE)' instead of 'make'. This has better behavior with GNU 'make' and -j. --- Makefile | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/Makefile b/Makefile index 6f70979..8d624bc 100644 --- a/Makefile +++ b/Makefile @@ -324,6 +324,8 @@ GZIPFLAGS= -9n ############################################################################### +#MAKE= make + cc= cc CC= $(cc) -DTZDIR=\"$(TZDIR)\" @@ -572,8 +574,8 @@ set-timestamps.out: $(ENCHILADA) # We also do an all-files run to catch links to links. check_public: $(ENCHILADA) - make maintainer-clean - make "CFLAGS=$(GCC_DEBUG_FLAGS)" $(ENCHILADA) all + $(MAKE) maintainer-clean + $(MAKE) "CFLAGS=$(GCC_DEBUG_FLAGS)" $(ENCHILADA) all mkdir tzpublic for i in $(TDATA) ; do \ $(zic) -v -d tzpublic $$i 2>&1 || exit; \ @@ -592,8 +594,8 @@ check_time_t_alternatives: zones=`$(AWK) '/^[^#]/ { print $$3 }'