From 345b6addf7195d39e86827aca9c16f0407aba028 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 7 Sep 2016 15:43:17 -0700 Subject: 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.) --- ltac/profile_ltac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ltac/profile_ltac.ml') diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 3661fe54f..50f9583f9 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 () -- cgit v1.2.3