diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2016-09-11 15:49:50 -0700 |
|---|---|---|
| committer |  Jason Gross <jgross@mit.edu> | 2016-09-11 19:13:39 -0400 |
| commit | 74d2ef26ce991c16039db8c06f813836304c6480 (patch) | |
| tree | ea0a157a47cea0a833ebcfc60cff3a4b36f0b31a /ltac | |
| parent | 345b6addf7195d39e86827aca9c16f0407aba028 (diff) | |
Fix newlines in printout of LtacProf
Previously, newlines were missing if a node had no children.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/profile_ltac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 50f9583f9..d2b7c7075 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -160,6 +160,7 @@ let rec print_node ~filter all_total indent prefix (s, e) = ++ padl 8 (string_of_int e.ncalls) ++ padl 10 (format_sec (e.max_total)) ) ++ + fnl () ++ print_table ~filter all_total indent false e.children and print_table ~filter all_total indent first_level table = @@ -179,7 +180,7 @@ and print_table ~filter all_total indent first_level table = let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in print_node ~filter all_total (indent ^ sep0) (indent ^ sep1) in - prlist_with_sep fnl (fun pr -> pr) (list_iter_is_last iter ls) + prlist (fun pr -> pr) (list_iter_is_last iter ls) let to_string ~filter node = let tree = node.children in @@ -224,7 +225,6 @@ let to_string ~filter node = header ++ print_table ~filter all_total "" true flat_tree ++ fnl () ++ - fnl () ++ header ++ print_table ~filter all_total "" true tree in |