From 56c3883b28c6c28466b7ed07b0e884d0242a5048 Mon Sep 17 00:00:00 2001 From: Paul-Elliot Date: Fri, 29 Sep 2023 12:55:03 +0200 Subject: [PATCH] Driver: make it deterministic again Signed-off-by: Paul-Elliot --- doc/driver.mld | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) *) ]}