diff options
| author | Hugo Herbelin | 2017-09-29 12:36:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-23 19:22:19 +0100 |
| commit | f36ea3ffb4ef01572db437392174f10650bee67b (patch) | |
| tree | db194ce33918caef9abe3496a7b1d86cca34c2f4 /kernel/type_errors.ml | |
| parent | 0b069d43bd673341f5f115d21b7bb805d485a5ae (diff) | |
Unify style of comments in file CUnix.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions