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 /stm/asyncTaskQueue.ml | |
| 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.)
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions