diff options
| author | Jason Gross | 2016-09-07 15:43:17 -0700 |
|---|---|---|
| committer | Jason Gross | 2016-09-11 19:13:39 -0400 |
| commit | 345b6addf7195d39e86827aca9c16f0407aba028 (patch) | |
| tree | fc71d12051506cf3ae5b6900aa215d9a3a789fd4 | |
| parent | 650550fc95d5ba41da84e2003371522221e27734 (diff) | |
Revert the LtacProf tactic table header
This removes a space (making the final letter of the right-aligned columns line come right before the vertical separators, rather than overlapping them), and left-aligns "tactic", as it was in Tobias' original code, which I think is easier to read. (This way, the alignment of the headers matches the alignment of the entries.)
| -rw-r--r-- | ltac/profile_ltac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 3661fe54f2..50f9583f94 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -147,7 +147,7 @@ let rec list_iter_is_last f = function | x :: xs -> f false x :: list_iter_is_last f xs let header = - str " tactic local total calls max" ++ + str " tactic local total calls max " ++ fnl () ++ str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘" ++ fnl () |