diff options
| author | Pierre Letouzey | 2015-11-28 10:16:54 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2015-12-12 18:51:37 +0100 |
| commit | 5550d920b831ec080cac236840132770bf1ba754 (patch) | |
| tree | 6e999655c8a3ceee2d407e910a145072afa98e37 /kernel/type_errors.ml | |
| parent | 72bb3992d912df33bac34f3a1c21989edcf9aa02 (diff) | |
Extraction: avoid generating some blanks at end-of-line
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions