From 7941c77b0aba5463ceb77054ea8dc5b3657a8742 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dag-Erling=20Sm=C3=B8rgrav?= Date: Sun, 23 Feb 2003 12:39:25 +0000 Subject: [PATCH] Don't try to build LINT if there is no NOTES file. --- tools/tools/tinderbox/tinderbox.pl | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tools/tools/tinderbox/tinderbox.pl b/tools/tools/tinderbox/tinderbox.pl index bea8d3a8e3a..fbcebfc6918 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");