diff options
| -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 bea8d3a..fbcebfc 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"); |
