config/tools.in
changeset 1854 02b74bd4373f
parent 1853 8676886c1ca9
child 1855 73917704e1d7
     1.1 --- a/config/tools.in	Mon Mar 15 22:02:02 2010 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,3 +0,0 @@
     1.4 -menu "Tools facilities"
     1.5 -source config.gen/tools.in
     1.6 -endmenu