From 4dcc092204f26668eab762bae3b04da3bc9007b5 Mon Sep 17 00:00:00 2001 From: phk Date: Sat, 14 Oct 2000 08:40:47 +0000 Subject: [PATCH] Duh! LINT is called NOTES these days. Make sure LINT checks profiling code as well. --- sys/conf/NOTES | 4 ++++ sys/i386/conf/NOTES | 4 ++++ sys/i386/conf/makeLINT.pl | 1 + 3 files changed, 9 insertions(+) diff --git a/sys/conf/NOTES b/sys/conf/NOTES index f965941bff98..180325426b82 100644 --- a/sys/conf/NOTES +++ b/sys/conf/NOTES @@ -33,6 +33,10 @@ ident LINT # maxusers 10 +# +# We want LINT to cover profiling as well +profile 1 + # # The `makeoptions' parameter allows variables to be passed to the # generated Makefile in the build area. diff --git a/sys/i386/conf/NOTES b/sys/i386/conf/NOTES index f965941bff98..180325426b82 100644 --- a/sys/i386/conf/NOTES +++ b/sys/i386/conf/NOTES @@ -33,6 +33,10 @@ ident LINT # maxusers 10 +# +# We want LINT to cover profiling as well +profile 1 + # # The `makeoptions' parameter allows variables to be passed to the # generated Makefile in the build area. diff --git a/sys/i386/conf/makeLINT.pl b/sys/i386/conf/makeLINT.pl index 06af090c9eff..3c0f917d057d 100644 --- a/sys/i386/conf/makeLINT.pl +++ b/sys/i386/conf/makeLINT.pl @@ -14,6 +14,7 @@ while (<>) { next if ($key =~ /^hint\./); if ($key eq "machine" || $key eq "ident" || $key eq "device" || $key eq "makeoptions" || $key eq "options" || + $key eq "profile" || $key eq "cpu" || $key eq "option" || $key eq "maxusers") { print "$line\n"; } else {