d42c1ee5c3
problem with having more CPUs than NCPU. PR: kern/4255 Submitted by: peter
problem with having more CPUs than NCPU. PR: kern/4255 Submitted by: peter