diff -r 8676886c1ca9 -r 02b74bd4373f config/tools.in
--- a/config/tools.in	Mon Mar 15 22:02:02 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-menu "Tools facilities"
-source config.gen/tools.in
-endmenu