diff options
Diffstat (limited to 'nuttx/tools')
| -rwxr-xr-x | nuttx/tools/configure.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/nuttx/tools/configure.sh b/nuttx/tools/configure.sh index a13e288be..84a9acb43 100755 --- a/nuttx/tools/configure.sh +++ b/nuttx/tools/configure.sh @@ -165,4 +165,10 @@ if [ ! -z "${appdir}" ]; then echo "CONFIG_APPS_DIR=\"$appdir\"" >> "${TOPDIR}/.configX" fi fi + +# install the final .configX only if it differs from the existing +# .config file. + install -C "${TOPDIR}/.configX" "${TOPDIR}/.config" +rm -f "${TOPDIR}/.configX" + |