diff options
Diffstat (limited to 'GNUmakefile')
| -rw-r--r-- | GNUmakefile | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/GNUmakefile b/GNUmakefile index 22c57f5cb5b..b4b33f4dbb6 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -55,7 +55,9 @@ else # Once 'configure' exists, run it. # Finally, run the actual 'make'. -default $(filter-out configure Makefile,$(MAKECMDGOALS)): Makefile +ORDINARY_GOALS = $(filter-out configure Makefile bootstrap,$(MAKECMDGOALS)) + +default $(ORDINARY_GOALS): Makefile $(MAKE) -f Makefile $(MAKECMDGOALS) # Execute in sequence, so that multiple user goals don't conflict. .NOTPARALLEL: @@ -72,5 +74,11 @@ Makefile: configure ./configure @echo >&2 'Makefile built.' +# 'make bootstrap' in a fresh checkout needn't run 'configure' twice. +bootstrap: Makefile + $(MAKE) -f Makefile all + +.PHONY: bootstrap default $(ORDINARY_GOALS) + endif endif |