diff --git a/build/configure.sh b/build/configure.sh index 6e9ff35246a3eb847a9c7d1fd926a4315bae61f1..96ef0a80856069f10b3128b4f768baab60fd2fcb 100755 --- a/build/configure.sh +++ b/build/configure.sh @@ -912,6 +912,7 @@ fi # Print a summary of configuration options echo "INFO: optimization level is ${CXX_OPT}." +echo "INFO: optimization level is ${CXX_OPT}." >> configure.log if [ "x${CXX_DBG}" = "x" ]; then echo "INFO: gdb is disabled." echo "INFO: gdb is disabled." >> configure.log