diff --git a/tools/mkconfig.c b/tools/mkconfig.c index 307e7381d5d..579e29df00a 100644 --- a/tools/mkconfig.c +++ b/tools/mkconfig.c @@ -132,7 +132,7 @@ int main(int argc, char **argv, char **envp) printf("# define CONFIG_RR_INTERVAL 0\n"); printf("#endif\n\n"); - printf("/* The correct way to disable filesystem supuport is to set the number of\n"); + printf("/* The correct way to disable filesystem support is to set the number of\n"); printf(" * file descriptors to zero.\n"); printf(" */\n\n"); printf("#ifndef CONFIG_NFILE_DESCRIPTORS\n"); @@ -220,10 +220,18 @@ int main(int argc, char **argv, char **envp) printf("# define CONFIG_DISABLE_MQUEUE 1\n"); printf("#endif\n\n"); + printf("/* The correct way to disable socket support is to set the number of\n"); + printf(" * socket descriptors to zero.\n"); + printf(" */\n\n"); + printf("#ifndef CONFIG_NSOCKET_DESCRIPTORS\n"); + printf("# define CONFIG_NSOCKET_DESCRIPTORS 0\n"); + printf("#endif\n\n"); + printf("/* There can be no network support with no socket descriptors */\n\n"); printf("#if CONFIG_NSOCKET_DESCRIPTORS <= 0\n"); printf("# undef CONFIG_NET\n"); printf("#endif\n\n"); + printf("/* Conversely, if there is no network support, there is no need for\n"); printf(" * socket descriptors\n"); printf(" */\n\n");