diff -r 1cca90ce0481 -r dc17e615de2c kconfig/menu.c
--- a/kconfig/menu.c	Fri Oct 17 12:47:53 2008 +0000
+++ b/kconfig/menu.c	Thu Nov 13 17:55:16 2008 +0000
@@ -128,8 +128,14 @@
 	prop->visible.expr = menu_check_dep(dep);
 
 	if (prompt) {
-		if (isspace(*prompt)) {
-			prop_warn(prop, "leading whitespace ignored");
+		/* For crostool-NG, a leading pipe followed with spaces
+		 * means that pipe shall be removed, and the spaces should
+		 * not be trimmed.
+		 */
+		if (*prompt == '|')
+			prompt++;
+		else if (isspace(*prompt)) {
+			/* Silently trim leading spaces */
 			while (isspace(*prompt))
 				prompt++;
 		}