diff options
Diffstat (limited to 'GNUmakefile')
| -rw-r--r--[l---------] | GNUmakefile | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/GNUmakefile b/GNUmakefile index 0f24a727ed..b8bfc3528b 120000..100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -1 +1,13 @@ -GNUmakefile
\ No newline at end of file +# This file is a hack to let us pass whatever flags we want to Make, +# since adjusting MAKEFLAGS at runtime only half-works. +# +# Most of the complexity is dancing around to avoid having any +# possibly conflicting identifiers. + +MAKEFLAGS += --no-print-directory +rest = $(wordlist 2,$(words $1),$1) +target = $(or $(firstword $(MAKECMDGOALS)),default) +$(target): + @+$(MAKE) -f Makefile --no-builtin-rules --no-builtin-variables --warn-undefined-variables $(MAKECMDGOALS) +$(or $(call rest,$(MAKECMDGOALS)),_$(target)): $(target) + @: |