diff options
Diffstat (limited to 'GNUmakefile')
-rw-r--r-- | GNUmakefile | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/GNUmakefile b/GNUmakefile index 5155487de28..76fd77ba1b0 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -104,8 +104,13 @@ configure: Makefile: configure @echo >&2 'There seems to be no Makefile in this directory.' +ifeq ($(configure),default) @echo >&2 'Running ./configure ...' ./configure +else + @echo >&2 'Running ./configure '$(configure)'...' + ./configure $(configure) +endif @echo >&2 'Makefile built.' # 'make bootstrap' in a fresh checkout needn't run 'configure' twice. |