diff options
| author | Dag-Erling Smørgrav <des@FreeBSD.org> | 2003-02-23 12:39:25 +0000 |
|---|---|---|
| committer | Dag-Erling Smørgrav <des@FreeBSD.org> | 2003-02-23 12:39:25 +0000 |
| commit | 7941c77b0aba5463ceb77054ea8dc5b3657a8742 (patch) | |
| tree | 5c103d5e5d9a7501b040bd5cbe9f14f0ebeb6080 /tools | |
| parent | aefdeea603d35a5c0653cbe6ebcf7d411d92f68d (diff) | |
Notes
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/tools/tinderbox/tinderbox.pl | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tools/tools/tinderbox/tinderbox.pl b/tools/tools/tinderbox/tinderbox.pl index bea8d3a8e3a54..fbcebfc691806 100644 --- a/tools/tools/tinderbox/tinderbox.pl +++ b/tools/tools/tinderbox/tinderbox.pl @@ -419,6 +419,10 @@ MAIN:{ } # Build LINT if requested + if ($cmds{'lint'} && ! -f "$sandbox/src/sys/$machine/conf/NOTES") { + logstage("no NOTES, skipping lint kernel"); + $cmds{'lint'} = 0; + } if ($cmds{'lint'}) { logstage("building lint kernel"); cd("$sandbox/src/sys/$machine/conf"); |