diff options
| -rw-r--r-- | tools/menuconfig.py | 15 |
1 files changed, 2 insertions, 13 deletions
diff --git a/tools/menuconfig.py b/tools/menuconfig.py index 96846b9ff2..2550424802 100644 --- a/tools/menuconfig.py +++ b/tools/menuconfig.py @@ -264,18 +264,7 @@ def pyconfig_silent(RTT_ROOT): fn = '.config' - if os.path.isfile(fn): - mtime = os.path.getmtime(fn) - else: - mtime = -1 - pymenuconfig.main(['--kconfig', 'Kconfig', '--config', '.config', '--silent', 'True']) - if os.path.isfile(fn): - mtime2 = os.path.getmtime(fn) - else: - mtime2 = -1 - - # make rtconfig.h - if mtime != mtime2: - mk_rtconfig(fn) + # silent mode, force to make rtconfig.h + mk_rtconfig(fn) |