diff options
| author | Paul Eggert <eggert@cs.ucla.edu> | 2014-04-16 23:40:25 -0700 |
|---|---|---|
| committer | Paul Eggert <eggert@cs.ucla.edu> | 2014-04-16 23:40:25 -0700 |
| commit | a3f989d4c430f4788352b2bad801ba99ccf2bb21 (patch) | |
| tree | 1aa551802fb10c8f5cad3a8ba0aca3d239f27305 /GNUmakefile | |
| parent | 8ac457d5edccc6cb72be90f1d8efc7389d1c824c (diff) | |
* GNUmakefile: Speed up 'make bootstrap' in fresh checkout.
(ORDINARY_GOALS): New macro, which excludes 'bootstrap'.
(bootstrap, .PHONY): New rules.
* INSTALL.REPO: Document current procedure better.
Move copyright notice to just before license notice.
Diffstat (limited to 'GNUmakefile')
| -rw-r--r-- | GNUmakefile | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/GNUmakefile b/GNUmakefile index 22c57f5cb5..b4b33f4dbb 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 |