diff options
Diffstat (limited to 'comfignat.mk')
| -rw-r--r-- | comfignat.mk | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/comfignat.mk b/comfignat.mk index d24a262..d138c85 100644 --- a/comfignat.mk +++ b/comfignat.mk @@ -412,16 +412,20 @@ configure:: ${if ${or ${findstring command line, \ ${origin ${variable}}}, \ ${filter true,${${variable}_is_configured}}}, \ - echo '${variable} = ${value ${variable}}'; \ + echo 'ifneq "$${origin ${variable}}" "command line"';\ + echo 'override ${variable} = ${value ${variable}}'; \ + echo 'endif'; \ echo '${variable}_is_configured = true';}} \ ) > comfignat_configuration.mk # Out of the variables listed in configuration_variables, all that were # overridden on the command line, and all that were previously configured, are -# written to the configuration file. A variable is considered previously -# configured if there is another variable with "_is_configured" appended to its -# name and a value of "true". Such a variable is also written for each -# configured variable. It is therefore possible to delete a variable V from the -# configuration by running "make configure V_is_configured=false". +# written to the configuration file. Configured values override defaults +# defined later in the containing makefile, but can be overridden on the +# command line. A variable is considered previously configured if there is +# another variable with "_is_configured" appended to its name and a value of +# "true". Such a variable is also written for each configured variable. It is +# therefore possible to delete a variable V from the configuration by running +# "make configure V_is_configured=false". comfignat.gpr: comfignat.gpr.gp "${GNATPREP}" $< $@ -DInvoked_By_Makefile ${all_directories} |