Jonathan Gibbons Today at 10:40 AM
The file doc/building.html says to use make print-configure to show the command line used for your current configuration. make says there is no such rule.

5 replies

Mikael Vidstedt 1 minute ago
Looks like it’s print-configuration

Jonathan Gibbons 1 minute ago
thanks

Mikael Vidstedt 1 minute ago
Can you open a bug?

Jonathan Gibbons 1 minute ago
will do

Mikael Vidstedt < 1 minute ago
Looks like the docs have it right in 2 out of 3 places