diff options
| author | Hugo Herbelin | 2016-11-05 12:09:14 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-11-05 12:27:11 +0100 |
| commit | ed2ec9362c0c0010b9caaaba4dcc771878ee2b7c (patch) | |
| tree | 094df4df5fd4ebeff5f77fe8caac31f996aa2922 /kernel/nativelambda.mli | |
| parent | 0ad6edc1d088385ffe90f1a4dd1bddc04cb31b07 (diff) | |
Removing a special treatment for empty lines in comments.
This made the whole pp code complicated only for the purpose of the
beautifier, while it is not clear when this was useful.
Removing the code for simplicity, not excluding to later address
beautifier issues when they show up.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions