diff options
| -rw-r--r-- | sys/conf/NOTES | 4 | ||||
| -rw-r--r-- | sys/i386/conf/NOTES | 4 | ||||
| -rw-r--r-- | sys/i386/conf/makeLINT.pl | 1 |
3 files changed, 9 insertions, 0 deletions
diff --git a/sys/conf/NOTES b/sys/conf/NOTES index f965941..1803254 100644 --- a/sys/conf/NOTES +++ b/sys/conf/NOTES @@ -34,6 +34,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 f965941..1803254 100644 --- a/sys/i386/conf/NOTES +++ b/sys/i386/conf/NOTES @@ -34,6 +34,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 06af090..3c0f917 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 { |
