Save even environment variables in the configuration file.

1 files changed, 8 insertions, 5 deletions

diff --git a/manual.en.html b/manual.en.html
index 70703e4..a9d125a 100755
--- a/manual.en.html
+++ b/manual.en.html
@@ -425,11 +425,14 @@ your default.</p>
 
 <p>Those Make variables that installing users are expected to change can be
 configured persistently. Run "<samp>make configure</samp>" with some variables
-set on the command line. Those variables will then be saved in a file named
-<var>comfignat_configuration.mk</var>, which will be loaded in all subsequent
-Make invocations. Additional variables can be configured incrementally. The
-configuration can be erased with "<samp>make unconfigure</samp>" or as a part
-of "<samp>make distclean</samp>".</p>
+set on the command line or in the environment. Those variables will then be
+saved in a file named <var>comfignat_configuration.mk</var>, which will be
+loaded in all subsequent Make invocations. Additional variables can be
+configured incrementally. In subsequent Make invocations environment variables
+override values that were configured from the environment, and variables set on
+the command line override all configured values. The configuration can be
+erased with "<samp>make unconfigure</samp>" or as a part of
+"<samp>make distclean</samp>".</p>
 
 <p>The variables that can be configured are listed in the variable
 <var>configuration_variables</var>. The variables listed in <var>options</var>