diff options
| author | Jason Gross | 2016-09-17 13:05:11 -0700 |
|---|---|---|
| committer | GitHub | 2016-09-17 13:05:11 -0700 |
| commit | 2008e95eb33ccfdd191afc0d3f692772c077b7a4 (patch) | |
| tree | 2d30d787cd8c64001044b4385c604f6cf3b4f7e2 /kernel/type_errors.ml | |
| parent | f1a561d847e207433a0ec3e6333798dfa19e4a0c (diff) | |
Fix indentation of -profile-ltac in -help
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions