Hi Zhonghao, > It seems like there should be a file "menuconfig" or some other > similar object I can modify. But I cannot find such an object. I > would appreciate if you could give me any suggestions. Thank you!
Some of the information on that page is somewhat out of date, as we've since moved from a Kconfig/Kbuild build system to a CMake-based build system. So to enable the benchmarks, you would first have to 'cd' into your build directory where you once called the 'init-build.sh' or 'griddle' script. Then using 'ccmake' or similar, change the 'KernelBenchmarks' config option to either: 'generic', 'track_kernel_entries', 'tracepoints', or 'track_utilisation', depending on whatever you wish to benchmark. Sorry for any inconveniences, we'll update the page within a day or two. Sincerely, Damon _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
