diff options
| -rw-r--r-- | ltac/profile_ltac.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 7a8ef32c3f..422f916936 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -219,7 +219,8 @@ let rec list_iter_is_last f = function let header = str " tactic self total calls max" ++ fnl () ++ - str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘" + str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘" ++ + fnl () let rec print_node all_total indent prefix (s, n) = let e = n.entry in |