Skip to content

Commit

Permalink
Driver: make it deterministic again
Browse files Browse the repository at this point in the history
Signed-off-by: Paul-Elliot <[email protected]>
  • Loading branch information
panglesd committed Sep 29, 2023
1 parent 8794f54 commit 56c3883
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions doc/driver.mld
Original file line number Diff line number Diff line change
Expand Up @@ -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) *)
]}
Expand Down

0 comments on commit 56c3883

Please sign in to comment.