diff options
Diffstat (limited to 'Makeconfig')
| -rw-r--r-- | Makeconfig | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/Makeconfig b/Makeconfig index 4d6e2e6c54..37839bc972 100644 --- a/Makeconfig +++ b/Makeconfig @@ -149,6 +149,17 @@ ifeq ($(origin prefix),undefined) # ifndef would override explicit empty value. prefix = /usr/local endif +# Decide whether we shall build the programs or not. We always do this +# unless the user tells us (in configparms) or we are building for a +# standalone target. +ifndef build-programs +ifneq ($(config-os),none) +build-programs=yes +else +build-programs=no +endif +endif + # Common prefix for machine-dependent installation directories. ifeq ($(origin exec_prefix),undefined) exec_prefix = $(prefix) |