diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2016-06-16 07:22:00 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-06-16 07:22:00 -0400 |
| commit | 2dee12d9381ed82f81a63cf50f4d3f8f4eb5415c (patch) | |
| tree | a131e41ea7dafb1b1b1c2e8082a12d11e4e3be8c /ltac/profile_ltac.ml | |
| parent | a8c6eeeaa321a84063e8492aca25942a07c00ddb (diff) | |
Fix a printing typo
Introduced by b21fefc0ec0aab2560d0b654f1a1f4203898388b
Diffstat (limited to 'ltac/profile_ltac.ml')
| -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 7a8ef32c3..422f91693 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 |