diff options
| -rw-r--r-- | tools/tools/tinderbox/tinderbox.pl | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/tools/tools/tinderbox/tinderbox.pl b/tools/tools/tinderbox/tinderbox.pl index c46a0bf8342c..84ea09689705 100644 --- a/tools/tools/tinderbox/tinderbox.pl +++ b/tools/tools/tinderbox/tinderbox.pl @@ -415,8 +415,7 @@ MAIN:{ # Build GENERIC if requested if ($cmds{'generic'}) { logstage("building generic kernel"); - $ENV{'KERNCONF'} = "GENERIC"; - spawn('/usr/bin/make', 'buildkernel') + spawn('/usr/bin/make', 'buildkernel', 'KERNCONF=GENERIC') or error("failed to build generic kernel"); } @@ -427,8 +426,7 @@ MAIN:{ make('LINT') or error("failed to generate lint config"); cd("$sandbox/src"); - $ENV{'KERNCONF'} = "LINT"; - spawn('/usr/bin/make', 'buildkernel') + spawn('/usr/bin/make', 'buildkernel', 'KERNCONF=LINT') or error("failed to build lint kernel"); } |