diff --git a/doc/building.html b/doc/building.html index 0522bc4888b..4d5cdf67c3a 100644 --- a/doc/building.html +++ b/doc/building.html @@ -849,7 +849,7 @@ sudo mv /tmp/configure /usr/local/bin

If you update the repository and part of the configure script has changed, the build system will force you to re-run configure.

Most of the time, you will be fine by running configure again with the same arguments as the last time, which can easily be performed by make reconfigure. To simplify this, you can use the CONF_CHECK make control variable, either as make CONF_CHECK=auto, or by setting an environment variable. For instance, if you add export CONF_CHECK=auto to your .bashrc file, make will always run reconfigure automatically whenever the configure script has changed.

You can also use CONF_CHECK=ignore to skip the check for a needed configure update. This might speed up the build, but comes at the risk of an incorrect build result. This is only recommended if you know what you're doing.

-

From time to time, you will also need to modify the command line to configure due to changes. Use make print-configure to show the command line used for your current configuration.

+

From time to time, you will also need to modify the command line to configure due to changes. Use make print-configuration to show the command line used for your current configuration.

Using Fine-Grained Make Targets

The default behavior for make is to create consistent and correct output, at the expense of build speed, if necessary.

If you are prepared to take some risk of an incorrect build, and know enough of the system to understand how things build and interact, you can speed up the build process considerably by instructing make to only build a portion of the product.

diff --git a/doc/building.md b/doc/building.md index 926148d463d..69b7fe640e8 100644 --- a/doc/building.md +++ b/doc/building.md @@ -1556,8 +1556,8 @@ update. This might speed up the build, but comes at the risk of an incorrect build result. This is only recommended if you know what you're doing. From time to time, you will also need to modify the command line to `configure` -due to changes. Use `make print-configure` to show the command line used for -your current configuration. +due to changes. Use `make print-configuration` to show the command line used +for your current configuration. ### Using Fine-Grained Make Targets