config/companion_tools.in
changeset 3325 069f43a215cc
parent 3292 9321d9d7af9b
     1.1 --- a/config/companion_tools.in	Thu Feb 20 18:23:08 2014 +0000
     1.2 +++ b/config/companion_tools.in	Wed Jun 25 23:33:01 2014 +0200
     1.3 @@ -2,10 +2,14 @@
     1.4  
     1.5  menu "Companion tools"
     1.6  
     1.7 +# Tools that require make-3.81 to build should select this:
     1.8  config COMP_TOOLS_make_3_81_NEEDED
     1.9      bool
    1.10 +
    1.11 +config COMP_TOOLS_FORCE_make_3_81
    1.12 +    def_bool y
    1.13 +    depends on COMP_TOOLS_make_3_81_NEEDED
    1.14      depends on ! CONFIGURE_has_make381
    1.15 -    default y
    1.16      select COMP_TOOLS
    1.17      select COMP_TOOLS_make
    1.18