aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--ltac/profile_ltac.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index bea02e3dcb..fb71becfc3 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -235,7 +235,6 @@ let rec print_node all_total indent prefix (s, n) =
++ padl 8 (string_of_int e.ncalls)
++ padl 10 (format_sec (e.max_total))
) ++
- fnl () ++
print_table all_total indent false n.children
and print_table all_total indent first_level table =