diff --git a/doc/driver.mld b/doc/driver.mld index 012622ba48..d9040b3b40 100644 --- a/doc/driver.mld +++ b/doc/driver.mld @@ -789,11 +789,11 @@ If needed, the list of commands executed so far can be shown by de-commenting th # (* List.iter print_cmd (List.rev !commands);; *) ]} -Print the slowest commands for each subcommands: +If needed, the list of the slowest commands for each subcommands can be shown by de-commenting this block: (for the record, these commands are run from directory `_build/default/doc`) {[ -# List.iter print_cmd (k_longest_commands "compile" 5) +# (* List.iter print_cmd (k_longest_commands "compile" 5) *) # (* List.iter print_cmd (k_longest_commands "link" 5) *) # (* List.iter print_cmd (k_longest_commands "html-generate" 5) *) ]}