changeset 76041 | 4a1330addb4e |
parent 74840 | 4faf0ec33cbf |
child 76068 | 319d08115b13 |
--- a/etc/options Fri Sep 02 23:31:22 2022 +0200 +++ b/etc/options Fri Sep 02 23:19:02 2022 +0200 @@ -133,7 +133,7 @@ -- "build process output tail shown to user (in lines, 0 = unlimited)" option profiling : string = "" (standard "time") - -- "ML profiling (possible values: time, allocations)" + -- "ML profiling (possible values: time, time_thread, allocations)" option system_log : string = "" (standard "-") -- "output for system messages (log file or \"-\" for console progress)"